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.

Exact lookup

1. data RCSet a

   sbv	Data.SBV.Internals

   A RCSet is either a regular set or a set given by its complement from the corresponding universal set.

2. RegularSet :: Set a -> RCSet a

   sbv	Data.SBV.Internals

   No documentation available.

3. type SSet a = SBV RCSet a

   sbv	Data.SBV.Internals

   Symbolic Set. Note that we use RCSet, which supports both regular sets and complements, i.e., those obtained from the universal set (of the right type) by removing elements. Similar to SArray the contents are stored with object equality, which makes a difference if the underlying type contains IEEE Floats.

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

   sbv	Data.SBV.Internals

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

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

   sbv	Data.SBV.Internals

   No documentation available.

6. solverSetOptions :: SMTConfig -> [SMTOption]

   sbv	Data.SBV.Internals

   Options to set as we start the solver

7. supportsSets :: SolverCapabilities -> Bool

   sbv	Data.SBV.Internals

   Supports set operations?

8. supportsSets :: SolverCapabilities -> Bool

   sbv	Data.SBV.Internals

   Supports set operations?

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

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

Page 162 of many | Previous | Next