Nuprl Definition : seq-add

seq-add(s;x) ==  let n,f = s in <n + 1, λi.if i <z n then f i else x fi >


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  add: n + m,  natural_number: $n
Definitions occuring in definition :  apply: f a,  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  natural_number: $n,  add: n + m,  pair: <a, b>,  spread: spread def
FDL editor aliases :  seq-add
Latex:
seq-add(s;x)  ==    let  n,f  =  s  in  <n  +  1,  \mlambda{}i.if  i  <z  n  then  f  i  else  x  fi  >


Date html generated: 2018_07_25-PM-01_29_37
Last ObjectModification: 2018_06_19-AM-10_12_13

Theory : arithmetic


Home Index