Nuprl Definition : update-context3
update-context3(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-context3
Latex:
update-context3(X;v;t) == bind-provision(X;ctxt.ctxt; v:fst(t))
Date html generated:
2020_05_20-PM-08_13_40
Last ObjectModification:
2020_03_14-AM-10_25_31
Theory : cubical!type!theory
Home
Index