Nuprl Definition : num-antecedents
#f(e) == fix((λnum-antecedents,e. if f e = e then 0 else 1 + (num-antecedents (f e)) fi )) e
Definitions occuring in Statement :
es-eq-E: e = e',
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
FDL editor aliases :
num-antecedents
\#f(e) == fix((\mlambda{}num-antecedents,e. if f e = e then 0 else 1 + (num-antecedents (f e)) fi )) e
Date html generated:
2015_07_17-PM-00_54_40
Last ObjectModification:
2012_07_02-PM-04_10_58
Home
Index