Nuprl Definition : apply_gen
apply_gen(n;lst) == fix((λrec,m,g. if (m =z n) then g else rec (m + 1) (g (lst 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),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
add: n + m,
natural_number: $n,
apply: f a
FDL editor aliases :
apply_gen
Latex:
apply\_gen(n;lst) == fix((\mlambda{}rec,m,g. if (m =\msubz{} n) then g else rec (m + 1) (g (lst m)) fi ))
Date html generated:
2016_05_15-PM-03_03_36
Last ObjectModification:
2015_09_23-AM-07_41_28
Theory : bags
Home
Index