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