Nuprl Definition : qv-add

qv-add(as;bs) ==  fix((λqv-add,as,bs. if null(as) then as else [hd(as) + hd(bs) / (qv-add tl(as) tl(bs))] fi )) as bs


Definitions occuring in Statement :  qadd: r + s,  hd: hd(l),  null: null(as),  tl: tl(l),  cons: [a / b],  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x]
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  null: null(as),  cons: [a / b],  qadd: r + s,  hd: hd(l),  apply: f a,  tl: tl(l)
FDL editor aliases :  qv-add
Latex:
qv-add(as;bs)  ==
    fix((\mlambda{}qv-add,as,bs.  if  null(as)  then  as  else  [hd(as)  +  hd(bs)  /  (qv-add  tl(as)  tl(bs))]  fi  ))  as  b\000Cs


Date html generated: 2016_05_15-PM-11_20_09
Last ObjectModification: 2015_09_23-AM-08_28_39

Theory : rationals


Home Index