Nuprl Definition : recind-ycomb
Y' == λf,x. letrec x(y) = f x y in x(x)
Definitions occuring in Statement :
rec_ind: rec_ind def,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
rec_ind: rec_ind def,
apply: f a
FDL editor aliases :
ycomb'
Latex:
Y' == \mlambda{}f,x. letrec x(y) = f x y in x(x)
Date html generated:
2016_05_13-PM-03_04_37
Last ObjectModification:
2015_09_22-PM-05_43_41
Theory : core_2
Home
Index