Refinery.ProofState

Documentation

newtype ProofStateT ext m jdg

Constructors

ProofStateT

Fields

• unProofStateT :: Client jdg ext m ext

Instances

MonadState s m => MonadState s (ProofStateT ext m)

Defined in Refinery.ProofState

Methods

get :: ProofStateT ext m s

put :: s -> ProofStateT ext m ()

state :: (s -> (a, s)) -> ProofStateT ext m a

MonadReader env m => MonadReader env (ProofStateT ext m)

Defined in Refinery.ProofState

Methods

ask :: ProofStateT ext m env

local :: (env -> env) -> ProofStateT ext m a -> ProofStateT ext m a

reader :: (env -> a) -> ProofStateT ext m a

MonadError err m => MonadError err (ProofStateT ext m)

Defined in Refinery.ProofState

Methods

throwError :: err -> ProofStateT ext m a

catchError :: ProofStateT ext m a -> (err -> ProofStateT ext m a) -> ProofStateT ext m a

MonadProvable jdg m => MonadProvable jdg (ProofStateT ext m)

Defined in Refinery.Tactic.Internal

Methods

proving :: jdg -> ProofStateT ext m jdg

MonadTrans (ProofStateT ext)

Defined in Refinery.ProofState

Methods

lift :: Monad m => m a -> ProofStateT ext m a

Monad m => Monad (ProofStateT ext m)

Defined in Refinery.ProofState

Methods

(>>=) :: ProofStateT ext m a -> (a -> ProofStateT ext m b) -> ProofStateT ext m b

(>>) :: ProofStateT ext m a -> ProofStateT ext m b -> ProofStateT ext m b

return :: a -> ProofStateT ext m a

fail :: String -> ProofStateT ext m a

Monad m => Functor (ProofStateT ext m)

Defined in Refinery.ProofState

Methods

fmap :: (a -> b) -> ProofStateT ext m a -> ProofStateT ext m b

(<$) :: a -> ProofStateT ext m b -> ProofStateT ext m a

Monad m => Applicative (ProofStateT ext m)

Defined in Refinery.ProofState

Methods

pure :: a -> ProofStateT ext m a

(<*>) :: ProofStateT ext m (a -> b) -> ProofStateT ext m a -> ProofStateT ext m b

liftA2 :: (a -> b -> c) -> ProofStateT ext m a -> ProofStateT ext m b -> ProofStateT ext m c

(*>) :: ProofStateT ext m a -> ProofStateT ext m b -> ProofStateT ext m b

(<*) :: ProofStateT ext m a -> ProofStateT ext m b -> ProofStateT ext m a

MonadIO m => MonadIO (ProofStateT ext m)

Defined in Refinery.ProofState

Methods

liftIO :: IO a -> ProofStateT ext m a

MonadThrow m => MonadThrow (ProofStateT ext m)

Defined in Refinery.ProofState

Methods

throwM :: Exception e => e -> ProofStateT ext m a

MonadCatch m => MonadCatch (ProofStateT ext m)

Defined in Refinery.ProofState

Methods

catch :: Exception e => ProofStateT ext m a -> (e -> ProofStateT ext m a) -> ProofStateT ext m a

axiom :: Monad m => ext -> ProofStateT ext m jdg

mapExtract :: Monad m => (ext -> ext') -> (ext' -> ext) -> ProofStateT ext m jdg -> ProofStateT ext' m jdg