Nuprl Definition : rec_ind def
letrec x(y) = B[x; y] in x(A) == fix((λx,y. B[x; y])) A
Definitions occuring in Statement :
apply: f a,
fix: fix(F),
lambda: λx.A[x]
Definitions occuring in definition :
apply: f a,
fix: fix(F),
lambda: λx.A[x]
Latex:
letrec x(y) = B[x; y] in x(A) == fix((\mlambda{}x,y. B[x; y])) A
Date html generated:
2016_05_13-PM-03_04_05
Last ObjectModification:
2015_09_22-PM-01_26_54
Theory : core_1
Home
Index