Either package:sbv

Symbolic coproduct, symbolic version of Haskell's Either type.

Case analysis for symbolic Eithers. If the value isLeft, apply the first function; if it isRight, apply the second function.

>>> either (*2) (*3) (sLeft (3 :: SInteger))
6 :: SInteger

>>> either (*2) (*3) (sRight (3 :: SInteger))
9 :: SInteger

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

>>> let g = uninterpret "g" :: SInteger -> SInteger

>>> prove $ \x -> either f g (sLeft x) .== f x
Q.E.D.

>>> prove $ \x -> either f g (sRight x) .== g x
Q.E.D.

Symbolic version of the type Either.

Declare a symbolic maybe.

Declare a symbolic maybe, unnamed.

Declare a list of symbolic maybes.

Construct an SEither a b from an Either (SBV a) (SBV b)

>>> liftEither (Left 3 :: Either SInteger SBool)
Left 3 :: Either Integer Bool

>>> liftEither (Right sTrue :: Either SInteger SBool)
Right True :: Either Integer Bool