Email Gateway (Aug 22 2022 at 11:39): Email Gateway (Aug 22 2022 at 11:39):From: "W. Douglas Maurer" <maurer@email.gwu.edu>
Your question has an answer that is independent of any specific system such as Isabelle. Any sorting algorithm has a parameter which is a Boolean comparison function of two arguments. Let's call the function LEQ, and let's call the arguments A and B. Typically LEQ(A, B) returns true if A <= B in some sense, and it returns false otherwise. To do a reverse sort, simply redefine LEQ(A, B) to return true if A >= B in that same sense, and to return false otherwise. Now call your sort program with the new LEQ as its actual parameter, and you will automatically get a reverse sort.
Sent from my iPhone
Last updated: Apr 26 2024 at 16:20 UTC