Documentation.SBV.Examples.KnuckleDragger.AppendRev

Example use of the KnuckleDragger, on list append and reverses.

Documentation

data Elt

Use an uninterpreted type for the elements

Instances

Data Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.AppendRev

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Elt -> c Elt

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Elt

toConstr :: Elt -> Constr

dataTypeOf :: Elt -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Elt)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Elt)

gmapT :: (forall b. Data b => b -> b) -> Elt -> Elt

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Elt -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Elt -> r

gmapQ :: (forall d. Data d => d -> u) -> Elt -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Elt -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Elt -> m Elt

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Elt -> m Elt

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Elt -> m Elt

Read Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.AppendRev

Methods

readsPrec :: Int -> ReadS Elt

readList :: ReadS [Elt]

readPrec :: ReadPrec Elt

readListPrec :: ReadPrec [Elt]

Show Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.AppendRev

Methods

showsPrec :: Int -> Elt -> ShowS

show :: Elt -> String

showList :: [Elt] -> ShowS

SymVal Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.AppendRev

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Elt)

literal :: Elt -> SBV Elt

fromCV :: CV -> Elt

isConcretely :: SBV Elt -> (Elt -> Bool) -> Bool

free :: MonadSymbolic m => String -> m (SBV Elt)

free_ :: MonadSymbolic m => m (SBV Elt)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Elt]

symbolic :: MonadSymbolic m => String -> m (SBV Elt)

symbolics :: MonadSymbolic m => [String] -> m [SBV Elt]

unliteral :: SBV Elt -> Maybe Elt

isConcrete :: SBV Elt -> Bool

isSymbolic :: SBV Elt -> Bool

HasKind Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.AppendRev

Methods

kindOf :: Elt -> Kind

hasSign :: Elt -> Bool

intSizeOf :: Elt -> Int

isBoolean :: Elt -> Bool

isBounded :: Elt -> Bool

isReal :: Elt -> Bool

isFloat :: Elt -> Bool

isDouble :: Elt -> Bool

isRational :: Elt -> Bool

isFP :: Elt -> Bool

isUnbounded :: Elt -> Bool

isUserSort :: Elt -> Bool

isChar :: Elt -> Bool

isString :: Elt -> Bool

isList :: Elt -> Bool

isSet :: Elt -> Bool

isTuple :: Elt -> Bool

isMaybe :: Elt -> Bool

isEither :: Elt -> Bool

isArray :: Elt -> Bool

showType :: Elt -> String

SatModel Elt

Defined in Documentation.SBV.Examples.KnuckleDragger.AppendRev

Methods

parseCVs :: [CV] -> Maybe (Elt, [CV])

cvtModel :: (Elt -> Maybe b) -> Maybe (Elt, [CV]) -> Maybe (b, [CV])

type SElt = SBV Elt

Symbolic version of the type Elt.

appendNull :: IO Proof

xs ++ [] == xs

We have:

>>> appendNull
Lemma: appendNull                       Q.E.D.
[Proven] appendNull

consApp :: IO Proof

(x : xs) ++ ys == x : (xs ++ ys)

We have:

>>> consApp
Lemma: consApp                          Q.E.D.
[Proven] consApp

appendAssoc :: IO Proof

(xs ++ ys) ++ zs == xs ++ (ys ++ zs)

We have:

>>> appendAssoc
Lemma: appendAssoc                      Q.E.D.
[Proven] appendAssoc

reverseReverse :: IO Proof

reverse (reverse xs) == xs

We have:

>>> reverseReverse
Lemma: revApp                           Q.E.D.
Lemma: reverseReverse                   Q.E.D.
[Proven] reverseReverse