Idris2Doc : Control.Comonad.Env.Env

Control.Comonad.Env.Env

(source)

Definitions

recordEnvT : Type-> (Type->Type) ->Type->Type
Totality: total
Visibility: public export
Constructor: 
MkEnvT : e->wa->EnvTewa

Projections:
.env : EnvTewa->e
.val : EnvTewa->wa

Hints:
(Monoide, Applicativem) =>Applicative (EnvTem)
Comonadw=>Comonad (EnvTew)
(Semigroupe, ComonadApplyw) =>ComonadApply (EnvTew)
Comonadw=>ComonadEnve (EnvTew)
ComonadTrans (EnvTe)
Foldablew=>Foldable (EnvTew)
Functorw=>Functor (EnvTew)
Traversablew=>Traversable (EnvTew)
.env : EnvTewa->e
Totality: total
Visibility: public export
env : EnvTewa->e
Totality: total
Visibility: public export
.val : EnvTewa->wa
Totality: total
Visibility: public export
val : EnvTewa->wa
Totality: total
Visibility: public export
Env : Type->Type->Type
Totality: total
Visibility: public export
mkEnv : e->a->Envea
  Create an Env using an environment and a value

Totality: total
Visibility: public export
runEnv : Envea-> (e, a)
Totality: total
Visibility: public export
runEnvT : EnvTewa-> (e, wa)
Totality: total
Visibility: public export
local : (e->e') ->EnvTewa->EnvTe'wa
  Modifies the environment using the specified function.

Totality: total
Visibility: public export