record EnvT : Type -> (Type -> Type) -> Type -> Type- Totality: total
Visibility: public export
Constructor: MkEnvT : e -> w a -> EnvT e w a
Projections:
.env : EnvT e w a -> e .val : EnvT e w a -> w a
Hints:
(Monoid e, Applicative m) => Applicative (EnvT e m) Comonad w => Comonad (EnvT e w) (Semigroup e, ComonadApply w) => ComonadApply (EnvT e w) Comonad w => ComonadEnv e (EnvT e w) ComonadTrans (EnvT e) Foldable w => Foldable (EnvT e w) Functor w => Functor (EnvT e w) Traversable w => Traversable (EnvT e w)
.env : EnvT e w a -> e- Totality: total
Visibility: public export env : EnvT e w a -> e- Totality: total
Visibility: public export .val : EnvT e w a -> w a- Totality: total
Visibility: public export val : EnvT e w a -> w a- Totality: total
Visibility: public export Env : Type -> Type -> Type- Totality: total
Visibility: public export mkEnv : e -> a -> Env e a Create an Env using an environment and a value
Totality: total
Visibility: public exportrunEnv : Env e a -> (e, a)- Totality: total
Visibility: public export runEnvT : EnvT e w a -> (e, w a)- Totality: total
Visibility: public export local : (e -> e') -> EnvT e w a -> EnvT e' w a Modifies the environment using the specified function.
Totality: total
Visibility: public export