Nuprl Definition : str-to-nat-plus

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 occuring in Statement :  str1-to-nat: str1-to-nat(a) list_ind: list_ind apply: a lambda: λx.A[x] multiply: m add: m natural_number: $n
Definitions occuring in definition :  list_ind: list_ind lambda: λx.A[x] apply: a add: m str1-to-nat: str1-to-nat(a) multiply: 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: 2016_05_14-PM-03_35_32
Last ObjectModification: 2015_09_22-PM-06_01_14

Theory : decidable!equality

Home Index