Maybe package:sbv

Symbolic option type, symbolic version of Haskell's Maybe type.

Case analysis for symbolic Maybes. If the value isNothing, return the default value; if it isJust, apply the function.

>>> maybe 0 (`sMod` 2) (sJust (3 :: SInteger))
1 :: SInteger

>>> maybe 0 (`sMod` 2) (sNothing :: SMaybe Integer)
0 :: SInteger

>>> let f = uninterpret "f" :: SInteger -> SBool

>>> prove $ \x d -> maybe d f (sJust x) .== f x
Q.E.D.

>>> prove $ \d -> maybe d f sNothing .== d
Q.E.D.

Symbolic Maybe

Declare a named SMaybe. NB. For a version which generalizes over the underlying monad, see sMaybe

Declare an unnamed SMaybe. NB. For a version which generalizes over the underlying monad, see sMaybe_

Declare a list of SMaybe values. NB. For a version which generalizes over the underlying monad, see sMaybes

Maybe

Return the value of an optional value. The default is returned if Nothing. Compare to fromJust.

>>> fromMaybe 2 (sNothing :: SMaybe Integer)
2 :: SInteger

>>> fromMaybe 2 (sJust 5 :: SMaybe Integer)
5 :: SInteger

>>> prove $ \x -> fromMaybe x (sNothing :: SMaybe Integer) .== x
Q.E.D.

>>> prove $ \x -> fromMaybe (x+1) (sJust x :: SMaybe Integer) .== x
Q.E.D.

Construct an SMaybe a from a Maybe (SBV a).

>>> liftMaybe (Just (3 :: SInteger))
Just 3 :: SMaybe Integer

>>> liftMaybe (Nothing :: Maybe SInteger)
Nothing :: SMaybe Integer