Nuprl Definition : uncurry-gen
uncurry-gen(n) == fix((λrec,m,g. if (m =z n) then g else rec (m + 1) (λx.(g x (x m))) fi ))
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
add: n + m,
natural_number: $n,
lambda: λx.A[x],
apply: f a
FDL editor aliases :
uncurry-gen
Latex:
uncurry-gen(n) == fix((\mlambda{}rec,m,g. if (m =\msubz{} n) then g else rec (m + 1) (\mlambda{}x.(g x (x m))) fi ))
Date html generated:
2016_05_15-PM-03_02_49
Last ObjectModification:
2015_09_23-AM-07_41_21
Theory : bags
Home
Index