Hoogle Search

Within LTS Haskell 24.60 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

  1. isSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool

    sbv Data.SBV.Set

    Subset test. 

    >>> prove $ empty `isSubsetOf` (full :: SSet Integer)
Q.E.D.

    >>> prove $ \x (s :: SSet Integer) -> s `isSubsetOf` (x `insert` s)
Q.E.D.

    >>> prove $ \x (s :: SSet Integer) -> (x `delete` s) `isSubsetOf` s
Q.E.D.

  2. offsetIndexOf :: SString -> SString -> SInteger -> SInteger

    sbv Data.SBV.String

    offsetIndexOf s sub offset. Retrieves first position of sub at or after offset in s, -1 if there are no occurrences. 

    >>> prove $ \s sub -> offsetIndexOf s sub 0 .== indexOf s sub
Q.E.D.

>>> prove $ \s sub i -> i .>= length s .&& length sub .> 0 .=> offsetIndexOf s sub i .== -1
Q.E.D.

>>> prove $ \s sub i -> i .> length s .=> offsetIndexOf s sub i .== -1
Q.E.D.

  3. cgSetDriverValues :: [Integer] -> SBVCodeGen ()

    sbv Data.SBV.Tools.CodeGen

    Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.

  4. type ConstraintSet = Symbolic ()

    sbv Data.SBV.Trans

    A constraint set is a symbolic program that returns no values. The idea is that the constraints/min-max goals will serve as the collection of constraints that will be used for sat/optimize calls.

  5. KSet :: Kind -> Kind

    sbv Data.SBV.Trans

    No documentation available.

  6. isSet :: HasKind a => a -> Bool

    sbv Data.SBV.Trans

    No documentation available.

  7. sSetBitTo :: SFiniteBits a => SBV a -> SBV a -> SBool -> SBV a

    sbv Data.SBV.Trans

    Variant of setBitTo when the index is symbolic. If the index it out-of-bounds, then the result is underspecified.

  8. solverSetOptions :: SMTConfig -> [SMTOption]

    sbv Data.SBV.Trans

    Options to set as we start the solver

  9. checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])

    sbv Data.SBV.Trans.Control

    Generalization of checkSatAssumingWithUnsatisfiableSet

  10. resetAssertions :: (MonadIO m, MonadQuery m) => m ()

    sbv Data.SBV.Trans.Control

    Generalization of resetAssertions

Page 163 of many | Previous | Next