Nuprl Definition : seq-cons

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


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


Date html generated: 2018_07_25-PM-01_28_54
Last ObjectModification: 2018_06_12-PM-10_25_38

Theory : arithmetic


Home Index