Nuprl Definition : ctt_meaning
[[ctxt;t]] == Provisional''''(ctt-meaning-type{i:l}(context-set(ctxt);t)) supposing context-ok(ctxt)
Definitions occuring in Statement :
ctt-meaning-type: ctt-meaning-type{i:l}(X;t),
context-set: context-set(ctxt),
context-ok: context-ok(ctxt),
uimplies: b supposing a,
provisional-type: Provisional(T)
Definitions occuring in definition :
uimplies: b supposing a,
context-ok: context-ok(ctxt),
provisional-type: Error :provisional-type,
ctt-meaning-type: ctt-meaning-type{i:l}(X;t),
context-set: context-set(ctxt)
FDL editor aliases :
ctt_meaning
Latex:
[[ctxt;t]] ==
Provisional''''(ctt-meaning-type\{i:l\}(context-set(ctxt);t)) supposing context-ok(ctxt)
Date html generated:
2020_05_21-AM-10_33_11
Last ObjectModification:
2020_03_18-PM-02_46_09
Theory : cubical!type!theory
Home
Index