Nuprl Definition : ctt-is-term
ctt-is-term(t) == isvarterm(t) ∨bctt-op-sort(term-opr(t)) =a "term"
Definitions occuring in Statement :
ctt-op-sort: ctt-op-sort(f),
term-opr: term-opr(t),
isvarterm: isvarterm(t),
bor: p ∨bq,
eq_atom: x =a y,
token: "$token"
Definitions occuring in definition :
bor: p ∨bq,
isvarterm: isvarterm(t),
eq_atom: x =a y,
ctt-op-sort: ctt-op-sort(f),
term-opr: term-opr(t),
token: "$token"
FDL editor aliases :
ctt-is-term
Latex:
ctt-is-term(t) == isvarterm(t) \mvee{}\msubb{}ctt-op-sort(term-opr(t)) =a "term"
Date html generated:
2020_05_21-AM-10_34_35
Last ObjectModification:
2020_02_12-AM-11_14_59
Theory : cubical!type!theory
Home
Index