Nuprl Definition : nth_tl
nth_tl(n;as) == fix((λnth_tl,n,as. if n ≤z 0 then as else nth_tl (n - 1) tl(as) fi )) n as
Definitions occuring in Statement :
tl: tl(l),
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
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 ,
le_int: i ≤z j,
apply: f a,
subtract: n - m,
natural_number: $n,
tl: tl(l)
FDL editor aliases :
nth_tl
Latex:
nth\_tl(n;as) == fix((\mlambda{}nth$_{tl}$,n,as. if n \mleq{}z 0 then as else nth$_\mbackslash{}ff7\000Cbtl}$ (n - 1) tl(as) fi )) n as
Date html generated:
2016_05_14-AM-06_28_32
Last ObjectModification:
2015_12_03-PM-02_05_26
Theory : list_0
Home
Index