Nuprl Definition : from-upto
[n, m) == fix((λfrom-upto,n. if n <z m then [n / eval n' = n + 1 in from-upto n'] else [] fi )) n
Definitions occuring in Statement :
cons: [a / b],
nil: [],
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
lt_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 ,
lt_int: i <z j,
cons: [a / b],
callbyvalue: callbyvalue,
add: n + m,
natural_number: $n,
apply: f a,
nil: []
FDL editor aliases :
from-upto
Latex:
[n, m) == fix((\mlambda{}from-upto,n. if n <z m then [n / eval n' = n + 1 in from-upto n'] else [] fi )) n
Date html generated:
2016_05_14-PM-01_59_18
Last ObjectModification:
2015_09_22-PM-05_55_15
Theory : list_1
Home
Index