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/
You may get a better response on the mailing list; I’ve never actually tried that sort of thing with quicksort and there’s a lot to consider
-
-
Oh. I see. And what about mergesort? I’m working on a small presentation about the correctness powers of a language like Idris. QS isn’t really necessary, I’m mostly interested in proving properties of classic algorithms to the compiler.
-
merge sort might be easier - the important part either way would be defining what it means for a list to be sorted, I expect.
- 1 more reply
New conversation -
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.