Nuprl Definition : ctt-context-term-mng
ctt-context-term-mng{i:l}(X;t) ==
wfterm-accum(X;t)
ctxt,vs,v.cubical-context-lookup(ctxt;v)
ctxt,vs,f,L.ctt-op-meaning{i:l}(ctxt; vs; f; L)
p0,ws,op,sofar,bt.ctt-binder-context[p0;ws;op;sofar;bt]
Definitions occuring in Statement :
ctt-op-meaning: ctt-op-meaning{i:l}(X; vs; f; L),
ctt-binder-context: ctt-binder-context,
cubical-context-lookup: cubical-context-lookup(ctxt;v),
wfterm-accum: wfterm-accum,
so_apply: x[s1;s2;s3;s4;s5]
Definitions occuring in definition :
wfterm-accum: wfterm-accum,
cubical-context-lookup: cubical-context-lookup(ctxt;v),
ctt-op-meaning: ctt-op-meaning{i:l}(X; vs; f; L),
so_apply: x[s1;s2;s3;s4;s5],
ctt-binder-context: ctt-binder-context
FDL editor aliases :
ctt-context-term-mng
Latex:
ctt-context-term-mng\{i:l\}(X;t) ==
wfterm-accum(X;t)
ctxt,vs,v.cubical-context-lookup(ctxt;v)
ctxt,vs,f,L.ctt-op-meaning\{i:l\}(ctxt; vs; f; L)
p0,ws,op,sofar,bt.ctt-binder-context[p0;ws;op;sofar;bt]
Date html generated:
2020_05_21-AM-10_46_54
Last ObjectModification:
2020_03_16-PM-06_05_22
Theory : cubical!type!theory
Home
Index