Nuprl Definition : ctt-arity

ctt-arity(x) ==
  let k,v = x
  in if k =a "opid" then ctt-opid-arity(v)
     if k =a "nType" then []
     if k =a "nterm" then []
     else []
     fi

Definitions occuring in Statement : ctt-opid-arity: ctt-opid-arity(t), nil: [], ifthenelse: if b then t else f fi , eq_atom: x =a y, spread: spread def, token: "$token"
Definitions occuring in definition : spread: spread def, ctt-opid-arity: ctt-opid-arity(t), ifthenelse: if b then t else f fi , eq_atom: x =a y, token: "$token", nil: []
FDL editor aliases : ctt-arity

Latex:
ctt-arity(x) == let k,v = x in if k =a "opid" then ctt-opid-arity(v) if k =a "nType" then [] if k =a "nterm" then [] else [] fi Date html generated: 2020_05_20-PM-08_19_09 Last ObjectModification: 2020_02_25-PM-01_42_06 Theory : cubical!type!theory Home Index