tamarin-prover-utils- Utility library for the tamarin prover.

PortabilityGHC only
MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone




Computations that need perform case distinctions.


MonadDisj class

class Monad m => MonadDisj m whereSource


contradictoryBecause :: Maybe String -> m aSource

Mark a contradiction.

disjunction :: m a -> m a -> m aSource

Disjoin two computations.


contradictory :: MonadDisj m => m aSource

contradictory denotes the logical false.

contradictoryIf :: MonadDisj m => Bool -> m ()Source

contradictoryIf b is logically equivalent to not b

contradiction :: MonadDisj m => String -> m aSource

contradiction reason denotes the logical false, but also provides the reason as meta-information.

contradictionIf :: MonadDisj m => Bool -> String -> m ()Source

contradictionIf b reason is logically equivalent to not b, but also provides the reason as meta-information.

disjunctions :: MonadDisj m => [m a] -> m aSource

disjunctions ds builds the disjunction of all the ds values.

disjunctionOfList :: MonadDisj m => [a] -> m aSource

disjunctionOfList xs build the disjunction of the values in list xs.

The DisjT monad transformer

newtype DisjT m a Source

A disjunction of atoms of type a.




unDisjT :: ListT m a


MonadTrans DisjT 
MonadReader r m => MonadReader r (DisjT m) 
Monad m => Monad (DisjT m) 
Functor m => Functor (DisjT m) 
Applicative m => Applicative (DisjT m) 
Monad m => MonadDisj (DisjT m) 

disjT :: m [a] -> DisjT m aSource

Construct a DisjT action.

runDisjT :: DisjT m a -> m [a]Source

Run a DisjT action.

Convencience exports