Nuprl Definition : s-nth
s-nth(n;s) == fix((λs-nth,n,s. let a,s' = s in if (n =z 0) then a else eval m = n - 1 in s-nth m s' fi )) n s
Definitions occuring in Statement :
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
callbyvalue: callbyvalue,
subtract: n - m,
natural_number: $n,
apply: f a
FDL editor aliases :
s-nth
Latex:
s-nth(n;s) ==
fix((\mlambda{}s-nth,n,s. let a,s' = s in if (n =\msubz{} 0) then a else eval m = n - 1 in s-nth m s' fi )) n s
Date html generated:
2016_05_14-AM-06_22_41
Last ObjectModification:
2015_09_22-PM-05_47_55
Theory : co-recursion
Home
Index