Nuprl Definition : FAN
FAN(d) == bar_recursion(d;λn,s,f. 1;λn,s,f. (imax(f tt;f ff) + 1);0;λm.eval x = m in ⊥)
Definitions occuring in Statement :
imax: imax(a;b),
bar_recursion: bar_recursion,
callbyvalue: callbyvalue,
bottom: ⊥,
bfalse: ff,
btrue: tt,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
bar_recursion: bar_recursion,
add: n + m,
imax: imax(a;b),
btrue: tt,
apply: f a,
bfalse: ff,
natural_number: $n,
lambda: λx.A[x],
callbyvalue: callbyvalue,
bottom: ⊥
FDL editor aliases :
FAN
Latex:
FAN(d) == bar\_recursion(d;\mlambda{}n,s,f. 1;\mlambda{}n,s,f. (imax(f tt;f ff) + 1);0;\mlambda{}m.eval x = m in \mbot{})
Date html generated:
2019_06_20-AM-11_32_56
Last ObjectModification:
2019_01_27-PM-01_36_20
Theory : bool_1
Home
Index