Hi @edwinbrady, I’m learning Idris and I’d like to prove that QuickSort is correct.
I’ve taken as a base the partition function from the libs/prelude/Prelude/List.idr file.
From that, I built partByElem (partitions by comparing to an element) and
1/
merge sort might be easier - the important part either way would be defining what it means for a list to be sorted, I expect.
-
-
I’m currently doing it with a function (isSorted : List a -> Bool). Would it be easier with a type? Like SortedList, and proving that one can be built from (a) Single Elements and (b) Merging 2 SortedLists together?
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.