Hoogle Search
Within LTS Haskell 24.32 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
CUserSort :: (Maybe Int, String) -> CValsbv Data.SBV.Internals Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations
KUserSort :: String -> Maybe [String] -> Kindsbv Data.SBV.Internals No documentation available.
isUserSort :: HasKind a => a -> Boolsbv Data.SBV.Internals No documentation available.
supportsUninterpretedSorts :: SolverCapabilities -> Boolsbv Data.SBV.Internals Supports SMT-Lib2 style uninterpreted-sorts
supportsUninterpretedSorts :: SolverCapabilities -> Boolsbv Data.SBV.Internals Supports SMT-Lib2 style uninterpreted-sorts
KUserSort :: String -> Maybe [String] -> Kindsbv Data.SBV.Trans No documentation available.
isUserSort :: HasKind a => a -> Boolsbv Data.SBV.Trans No documentation available.
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.