---

str-to-nat-plus(s;n) ==
  rec-case(s) of [] => x.x | fst::rest => rec.x.(rec 
                                                   (str1-to-nat(fst)
                                                   + (10 * x))) 
  n

---

Definitions :  list_ind: rec-case(a) of [] => s | x::y => z.t[x; y; z],  lambda: x.A[x],  apply: f a,  add: n + m,  str1-to-nat: str1-to-nat(a),  multiply: n * m,  natural_number: $n
FDL editor aliases :  str-to-nat-plus

---

str-to-nat-plus(s;n)  ==
    rec-case(s)  of  []  =>  \mlambda{}x.x  |  fst::rest  =>  rec.\mlambda{}x.(rec  (str1-to-nat(fst)  +  (10  *  x)))  n


Date html generated: 2010_08_26-PM-11_30_34
Last ObjectModification: 2010_02_10-PM-02_28_56

Home Index