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 Either

Declare a named SEither. NB. For a version which generalizes over the underlying monad, see sEither

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

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

Disjoint union

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

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

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