Nuprl Definition : ctt-kind

ctt-kind(t) ==
  if isvarterm(t) then 0
  if ctt-op-sort(term-opr(t)) =a "fibrant" then 1
  if ctt-op-sort(term-opr(t)) =a "type" then 2
  else 0
  fi

Definitions occuring in Statement : ctt-op-sort: ctt-op-sort(f), term-opr: term-opr(t), isvarterm: isvarterm(t), ifthenelse: if b then t else f fi , eq_atom: x =a y, natural_number: $n, token: "$token"
Definitions occuring in definition : isvarterm: isvarterm(t), ifthenelse: if b then t else f fi , eq_atom: x =a y, ctt-op-sort: ctt-op-sort(f), term-opr: term-opr(t), token: "$token", natural_number: $n
FDL editor aliases : ctt-kind

Latex:
ctt-kind(t) == if isvarterm(t) then 0 if ctt-op-sort(term-opr(t)) =a "fibrant" then 1 if ctt-op-sort(term-opr(t)) =a "type" then 2 else 0 fi Date html generated: 2020_05_20-PM-08_17_47 Last ObjectModification: 2020_02_25-PM-01_17_18 Theory : cubical!type!theory Home Index