Nuprl Definition : ctt-term-is
ctt-term-is(s;t) == (¬bisvarterm(t)) ∧b let k,v = term-opr(t) in k =a "opid" ∧b v =a s
Definitions occuring in Statement :
term-opr: term-opr(t),
isvarterm: isvarterm(t),
band: p ∧b q,
bnot: ¬bb,
eq_atom: x =a y,
spread: spread def,
token: "$token"
Definitions occuring in definition :
bnot: ¬bb,
isvarterm: isvarterm(t),
spread: spread def,
term-opr: term-opr(t),
band: p ∧b q,
token: "$token",
eq_atom: x =a y
FDL editor aliases :
ctt-term-is
Latex:
ctt-term-is(s;t) == (\mneg{}\msubb{}isvarterm(t)) \mwedge{}\msubb{} let k,v = term-opr(t) in k =a "opid" \mwedge{}\msubb{} v =a s
Date html generated:
2020_05_20-PM-08_22_09
Last ObjectModification:
2020_02_15-AM-10_09_39
Theory : cubical!type!theory
Home
Index