Nuprl Definition : cubical-context-lookup

cubical-context-lookup(ctxt;v) == provision(in-context-dom(allow(ctxt);v); cubical_context_val(allow(ctxt);v))

Definitions occuring in Statement : cubical_context_val: cubical_context_val(ctxt;v), in-context-dom: in-context-dom(ctxt;v), allow: allow(x), provision: provision(ok; v)
Definitions occuring in definition : provision: Error :provision, in-context-dom: in-context-dom(ctxt;v), cubical_context_val: cubical_context_val(ctxt;v), allow: Error :allow
FDL editor aliases : cubical-context-lookup

Latex:
cubical-context-lookup(ctxt;v) == provision(in-context-dom(allow(ctxt);v); cubical\_context\_val(allow(ctxt);v)) Date html generated: 2020_05_20-PM-08_11_39 Last ObjectModification: 2020_03_18-PM-00_21_45 Theory : cubical!type!theory Home Index