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

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

Control.Monad.Disj

Contents

Description

Computations that need perform case distinctions.

Synopsis

MonadDisj class

class Monad m => MonadDisj m whereSource

Methods

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.

Constructors

DisjT 

Fields

unDisjT :: ListT m a
 

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

Construct a DisjT action.

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

Run a DisjT action.

Convencience exports