Nuprl Definition : ml-int-vec-add

ml-int-vec-add(as;bs) ==
  fix((λivadd,as,bs. if null(as) ∨bnull(bs)
                    then []
                    else let a.as2 = as 
                         in let b.bs2 = bs 
                            in [a + b / ivadd(as2)(bs2)]
                    fi ))(as)(bs)


Definitions occuring in Statement :  spreadcons: spreadcons,  ml_apply: f(x),  null: null(as),  cons: [a / b],  nil: [],  bor: p ∨bq,  ifthenelse: if b then t else f fi ,  fix: fix(F),  lambda: λx.A[x],  add: n + m
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  bor: p ∨bq,  null: null(as),  nil: [],  spreadcons: spreadcons,  cons: [a / b],  add: n + m,  ml_apply: f(x)
FDL editor aliases :  ml-int-vec-add
Latex:
ml-int-vec-add(as;bs)  ==
    fix((\mlambda{}ivadd,as,bs.  if  null(as)  \mvee{}\msubb{}null(bs)
                                        then  []
                                        else  let  a.as2  =  as 
                                                  in  let  b.bs2  =  bs 
                                                        in  [a  +  b  /  ivadd(as2)(bs2)]
                                        fi  ))(as)(bs)


Date html generated: 2017_09_29-PM-05_56_47
Last ObjectModification: 2017_05_19-PM-06_16_45

Theory : omega


Home Index