Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

[Tobias Nipkow]

Indeed, and that is consistent with informal language, eg "sorted by size". It looks like "wrt" is really better for relations.

Tobias

On 16/08/2017 17:04, Peter Lammich wrote:

However, sort_by takes a function mapping the elements into a linear order, which is less general than allowing arbitrary (preorder?) relations.

Peter


-------- Original Message --------

From: Makarius
To: Tobias Nipkow ,isabelle-dev@mailbroy.informatik.tu-muenchen.de
CC:


    On 16/08/17 16:10, Tobias Nipkow wrote:
     >
     > Concerning "sorted_by" vs "sorted_wrt": the latter seems closer to
     > informal usage. But if many people cry out for "by" we could change that.

    In Isabelle/ML we used to have "sort_wrt" for some decades, but I have
    changed that recently into into "sort_by" to make it coincide with the
    terminology of the Scala library.

    See
    http://isabelle.in.tum.de/repos/isabelle/rev/610794dff23c


    Makarius
    _______________________________________________
    isabelle-dev mailing list
    isabelle-...@in.tum.de
    https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Subject: Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev