Nuprl Definition : update-cubical-context2
ctxt; v:fst(T) == provision(allowed(T); let lvl,A,_ = allow(T) in update-context-lvl(ctxt;lvl;A;v))
Definitions occuring in Statement :
update-context-lvl: update-context-lvl(ctxt;lvl;T;v),
spreadn: spread3,
allow: allow(x),
allowed: allowed(x),
provision: provision(ok; v)
Definitions occuring in definition :
provision: Error :provision,
allowed: Error :allowed,
spreadn: spread3,
allow: Error :allow,
update-context-lvl: update-context-lvl(ctxt;lvl;T;v)
FDL editor aliases :
update-cubical-context2
Latex:
ctxt; v:fst(T) == provision(allowed(T); let lvl,A,$_{}$ = allow(T) in update-co\000Cntext-lvl(ctxt;lvl;A;v))
Date html generated:
2020_05_20-PM-08_10_19
Last ObjectModification:
2020_05_04-PM-01_11_19
Theory : cubical!type!theory
Home
Index