Nuprl Definition : ctt-term
CttTerm == wfterm(CttOp;λt.ctt-kind(t);λx.ctt-arity(x))
Definitions occuring in Statement :
ctt-arity: ctt-arity(x),
ctt-kind: ctt-kind(t),
ctt-op: CttOp,
wfterm: wfterm(opr;sort;arity),
lambda: λx.A[x]
Definitions occuring in definition :
wfterm: wfterm(opr;sort;arity),
ctt-op: CttOp,
ctt-kind: ctt-kind(t),
lambda: λx.A[x],
ctt-arity: ctt-arity(x)
FDL editor aliases :
ctt-term
Latex:
CttTerm == wfterm(CttOp;\mlambda{}t.ctt-kind(t);\mlambda{}x.ctt-arity(x))
Date html generated:
2020_05_20-PM-08_19_49
Last ObjectModification:
2020_02_25-PM-01_20_33
Theory : cubical!type!theory
Home
Index