Hoogle Search
Within LTS Haskell 24.51 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
mkSymbolicEnumeration :: Name -> Q [Dec]sbv Data.SBV Make an enumeration a symbolic type.
isAlphaNumL1 :: SChar -> SBoolsbv Data.SBV.Char Is this an alphabetical character or a digit? Only works for the Latin1 subset, otherwise returns sFalse.
>>> prove $ \c -> isAlphaNumL1 c .<=> isAlphaL1 c .|| isNumberL1 c Q.E.D.
-
sbv Data.SBV.Char Is this a number character? Only works for the Latin1 subset, otherwise returns sFalse.
-
sbv Data.SBV.Dynamic For each numeric value, show it in detail in the model with its bits spliced out. Good for floats.
crackNumSurfaceVals :: SMTConfig -> [(String, Integer)]sbv Data.SBV.Dynamic For crackNum: The surface representation of variables, if available
svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal]sbv Data.SBV.Dynamic Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus the lifting to Integers preserves the bounds; and then going back is just fine. So, things like [1, 5 .. 200] :: [SInt8] work just fine (end evaluate to empty list), since we see [1, 5 .. -56] in the Integer domain. Also note the explicit check for s /= f below to make sure we don't stutter and produce an infinite list.
svNumerator :: SVal -> Maybe Integersbv Data.SBV.Dynamic Grab the numerator of an SReal, if available
-
sbv Data.SBV.Internals PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.
-
sbv Data.SBV.Internals For each numeric value, show it in detail in the model with its bits spliced out. Good for floats.
crackNumSurfaceVals :: SMTConfig -> [(String, Integer)]sbv Data.SBV.Internals For crackNum: The surface representation of variables, if available