Nuprl Definition : cons-nat-seq

cons-nat-seq(n;a) ==  λk.if k=0  then n  else (a (k - 1))


Definitions occuring in Statement :  int_eq: if a=b  then c  else d,  apply: f a,  lambda: λx.A[x],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  natural_number: $n,  subtract: n - m,  apply: f a,  int_eq: if a=b  then c  else d,  lambda: λx.A[x]
FDL editor aliases :  cons-nat-seq
Latex:
cons-nat-seq(n;a)  ==    \mlambda{}k.if  k=0    then  n    else  (a  (k  -  1))


Date html generated: 2017_04_20-AM-07_35_21
Last ObjectModification: 2017_04_07-PM-05_51_51

Theory : continuity


Home Index