Hoogle Search

Within LTS Haskell 24.34 (ghc-9.10.3)

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

Exact lookup

1. offsetIndexOf :: (Eq a, SymVal a) => SList a -> SList a -> SInteger -> SInteger

   sbv	Data.SBV.List

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

   >>> prove $ \(l :: SList Int8) sub -> offsetIndexOf l sub 0 .== indexOf l sub
   Q.E.D.
   
   >>> prove $ \(l :: SList Int8) sub i -> i .>= length l .&& length sub .> 0 .=> offsetIndexOf l sub i .== -1
   Q.E.D.
   
   >>> prove $ \(l :: SList Int8) sub i -> i .> length l .=> offsetIndexOf l sub i .== -1
   Q.E.D.
   

2. isProperSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool

   sbv	Data.SBV.Set

   Proper subset test.

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

   >>> prove $ \x (s :: SSet Integer) -> s `isProperSubsetOf` (x `insert` s)
   Falsifiable. Counter-example:
   s0 = 2 :: Integer
   s1 = U :: {Integer}
   

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

   >>> prove $ \x (s :: SSet Integer) -> (x `delete` s) `isProperSubsetOf` s
   Falsifiable. Counter-example:
   s0 =         2 :: Integer
   s1 = U - {2,3} :: {Integer}
   

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

3. 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.
   

4. 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.
   

5. 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.

6. 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.

7. KSet :: Kind -> Kind

   sbv	Data.SBV.Trans

   No documentation available.

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

   sbv	Data.SBV.Trans

   No documentation available.

9. 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.

10. solverSetOptions :: SMTConfig -> [SMTOption]

    sbv	Data.SBV.Trans

    Options to set as we start the solver

Page 163 of many | Previous | Next