Nuprl Definition : update-cubical-context
ctxt; v: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),
spread: spread def,
allow: allow(x),
allowed: allowed(x),
provision: provision(ok; v)
Definitions occuring in definition :
provision: Error :provision,
allowed: Error :allowed,
spread: spread def,
allow: Error :allow,
update-context-lvl: update-context-lvl(ctxt;lvl;T;v)
FDL editor aliases :
update-cubical-context
Latex:
ctxt; v:T == provision(allowed(T); let lvl,A = allow(T) in update-context-lvl(ctxt;lvl;A;v))
Date html generated:
2020_05_20-PM-08_09_39
Last ObjectModification:
2020_05_04-PM-01_03_38
Theory : cubical!type!theory
Home
Index