Nuprl Definition : seq-tl
seq-tl(s) ==  let n,f = s in <n - 1, λi.(f (i + 1))>
Definitions occuring in Statement : 
apply: f a
, 
lambda: λx.A[x]
, 
spread: spread def, 
pair: <a, b>
, 
subtract: n - m
, 
add: n + m
, 
natural_number: $n
Definitions occuring in definition : 
natural_number: $n
, 
add: n + m
, 
apply: f a
, 
lambda: λx.A[x]
, 
subtract: n - m
, 
pair: <a, b>
, 
spread: spread def
FDL editor aliases : 
seq-tl
Latex:
seq-tl(s)  ==    let  n,f  =  s  in  <n  -  1,  \mlambda{}i.(f  (i  +  1))>
Date html generated:
2018_07_25-PM-01_29_08
Last ObjectModification:
2018_06_15-PM-01_06_45
Theory : arithmetic
Home
Index