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