Nuprl Definition : update-tuple
update-tuple(len;x;n;y) ==
fix((λupdate-tuple,len,x,n. if (n =z 0)
then if (len =z 1) then y else <y, snd(x)> fi
else <fst(x), update-tuple (len - 1) (snd(x)) (n - 1)>
fi ))
len
x
n
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
pi1: fst(t),
pi2: snd(t),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
pair: <a, b>,
subtract: 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),
pair: <a, b>,
pi1: fst(t),
apply: f a,
pi2: snd(t),
subtract: n - m,
natural_number: $n
FDL editor aliases :
update-tuple
Latex:
update-tuple(len;x;n;y) ==
fix((\mlambda{}update-tuple,len,x,n. if (n =\msubz{} 0)
then if (len =\msubz{} 1) then y else <y, snd(x)> fi
else <fst(x), update-tuple (len - 1) (snd(x)) (n - 1)>
fi ))
len
x
n
Date html generated:
2016_05_14-PM-03_58_03
Last ObjectModification:
2015_09_22-PM-06_02_00
Theory : tuples
Home
Index