eneral than allowing arbitrary (preorder?) relations.
Peter
Original Message ----
Subject: Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added
Data_Structures/Binomial_Heap.thy
From: Makarius
To: Tobias Nipkow ,isabelle-dev@mailbroy.informatik.tu-muenchen.de
CC:
On 16
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 Subject: Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thyFrom:
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
I feel that take/drop_chain are too specialised for List, although of course
this is subjective.
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.
Tobias
On 16/08/2017 12:10, Christian Sternagel
Dear all,
speaking of "chain", for me the main motivation of introducing "linked
P" was in order to work well together with the corresponding
generalizations of "take_while" and "drop_while", which are called
"take_chain" and "drop_chain" in the AFP entry Efficient-Mergesort.
E.g., "take_chain
Hi Christian, Tobias,
> I think your "sorted_wrt" is almost (modulo "fun" vs. "inductive") my
> "linked" from the AFP (Efficient_Mergesort).
>
>
> https://www.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Sort.html
>
> Maybe we could unify the constants/names somehow?
>
>
