Hoogle Search
Within LTS Haskell 24.33 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
mkUninterpretedSort :: Name -> Q [Dec]sbv Data.SBV.Trans Make an uninterpred sort.
module Documentation.SBV.Examples.BitPrecise.
MergeSort Symbolic implementation of merge-sort and its correctness. Note that this version, while fully push-button, proves merge-sort correct for fixed number of elements, i.e., not in its generality. A general proof would require non-trivial applications of induction and more manual guiding. We do such a proof in Documentation.SBV.Examples.KnuckleDragger.MergeSort, which shows the full-power of the theorem-proving like aspects of SBV.
-
sbv Documentation.SBV.Examples.BitPrecise.MergeSort Simple merge-sort implementation. We simply divide the input list in two halves so long as it has at least two elements, sort each half on its own, and then merge.
module Documentation.SBV.Examples.KnuckleDragger.
InsertionSort Proving insertion sort correct.
insertionSort :: SList Integer -> SList Integersbv Documentation.SBV.Examples.KnuckleDragger.InsertionSort Insertion sort, using insert above to successively insert the elements.
module Documentation.SBV.Examples.KnuckleDragger.
MergeSort Proving merge sort correct.
mergeSort :: SList Integer -> SList Integersbv Documentation.SBV.Examples.KnuckleDragger.MergeSort Merge sort, using merge above to successively sort halved input
module Documentation.SBV.Examples.KnuckleDragger.
QuickSort Proving quick sort correct. The proof here closely follows the development given by Tobias Nipkow, in his paper "Term Rewriting and Beyond -- Theorem Proving in Isabelle," published in Formal Aspects of Computing 1: 320-338 back in 1989.
quickSort :: SList Integer -> SList Integersbv Documentation.SBV.Examples.KnuckleDragger.QuickSort Quick-sort, using the first element as pivot.
module Documentation.SBV.Examples.Uninterpreted.
UISortAllSat Demonstrates uninterpreted sorts and how all-sat behaves for them. Thanks to Eric Seidel for the idea.