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: f a,
lambda: λx.A[x],
multiply: n * m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
list_ind: list_ind,
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
Latex:
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