Nuprl Definition : provisional-monad
provisional-monad{i:l}() == mk_monad(λT.Provisional(T);λx.OK(x);λx,f. bind-provision(x;u.f u))
Definitions occuring in Statement :
bind-provision: bind-provision(x;t.f[t]),
provision: provision(ok; v),
provisional-type: Provisional(T),
mk_monad: mk_monad(M;return;bind),
true: True,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
mk_monad: mk_monad(M;return;bind),
provisional-type: Provisional(T),
provision: provision(ok; v),
true: True,
lambda: λx.A[x],
bind-provision: bind-provision(x;t.f[t]),
apply: f a
FDL editor aliases :
provisional-monad
Latex:
provisional-monad\{i:l\}() == mk\_monad(\mlambda{}T.Provisional(T);\mlambda{}x.OK(x);\mlambda{}x,f. bind-provision(x;u.f u))
Date html generated:
2020_05_20-AM-08_01_09
Last ObjectModification:
2020_05_17-PM-01_08_43
Theory : monads
Home
Index