Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Uninterpreted.Deduce

Contents

Representing uninterpreted booleans
Uninterpreted connectives over B
Demonstrated deduction

Description

Demonstrates uninterpreted sorts and how they can be used for deduction.

Synopsis

data B
cv2B :: String -> [CV] -> B
_undefiner_B :: a
type SB = SBV B
and :: SB -> SB -> SB
or :: SB -> SB -> SB
not :: SB -> SB
test :: IO ThmResult

Representing uninterpreted booleans

data B Source #

The uninterpreted sort B, corresponding to the carrier.

Instances

Instances details

Arbitrary B Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Deduce Methods arbitrary :: Gen B # shrink :: B -> [B] #
SymVal B Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Deduce Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV B) Source # mkSymValInit :: State -> SBV B -> IO () Source # literal :: B -> SBV B Source # fromCV :: CV -> B Source # isConcretely :: SBV B -> (B -> Bool) -> Bool Source # minMaxBound :: Maybe (B, B) Source # free :: MonadSymbolic m => String -> m (SBV B) Source # free_ :: MonadSymbolic m => m (SBV B) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV B] Source # symbolic :: MonadSymbolic m => String -> m (SBV B) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV B] Source # unliteral :: SBV B -> Maybe B Source # unlitCV :: SBV B -> Maybe (Kind, CVal) Source # isConcrete :: SBV B -> Bool Source # isSymbolic :: SBV B -> Bool Source #
HasKind B Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.Deduce Methods kindOf :: B -> Kind Source # hasSign :: B -> Bool Source # intSizeOf :: B -> Int Source # isBoolean :: B -> Bool Source # isBounded :: B -> Bool Source # isReal :: B -> Bool Source # isFloat :: B -> Bool Source # isDouble :: B -> Bool Source # isRational :: B -> Bool Source # isFP :: B -> Bool Source # isUnbounded :: B -> Bool Source # isADT :: B -> Bool Source # isChar :: B -> Bool Source # isString :: B -> Bool Source # isList :: B -> Bool Source # isSet :: B -> Bool Source # isTuple :: B -> Bool Source # isArray :: B -> Bool Source # isRoundingMode :: B -> Bool Source # isUninterpreted :: B -> Bool Source # showType :: B -> String Source #