Nuprl Definition : ml-select
ml-select(n;L) == fix((λselect,n,L. let x,y = L in if n <z 1 then x else select(n - 1)(y) fi ))(n)(L)
Definitions occuring in Statement :
ml_apply: f(x),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
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 ,
lt_int: i <z j,
ml_apply: f(x),
subtract: n - m,
natural_number: $n
FDL editor aliases :
ml-select
Latex:
ml-select(n;L) == fix((\mlambda{}select,n,L. let x,y = L in if n <z 1 then x else select(n - 1)(y) fi ))(n)(\000CL)
Date html generated:
2017_09_29-PM-05_51_24
Last ObjectModification:
2017_05_19-PM-05_49_35
Theory : ML
Home
Index