Nuprl Definition : update-context2
update-context2(X;v;t) == bind-provision(X;ctxt.ctxt; v:fst(t))
Definitions occuring in Statement :
update-cubical-context2: ctxt; v:fst(T),
bind-provision: bind-provision(x;t.f[t])
Definitions occuring in definition :
bind-provision: Error :bind-provision,
update-cubical-context2: ctxt; v:fst(T)
FDL editor aliases :
update-context2
Latex:
update-context2(X;v;t) == bind-provision(X;ctxt.ctxt; v:fst(t))
Date html generated:
2020_05_20-PM-08_12_19
Last ObjectModification:
2020_03_14-AM-09_57_42
Theory : cubical!type!theory
Home
Index