Nuprl Definition : str1-to-nat

str1-to-nat(a) ==
  if a =a "1" then 1
  if a =a "2" then 2
  if a =a "3" then 3
  if a =a "4" then 4
  if a =a "5" then 5
  if a =a "6" then 6
  if a =a "7" then 7
  if a =a "8" then 8
  if a =a "9" then 9
  else 0
  fi

Definitions occuring in Statement : ifthenelse: if b then t else f fi , eq_atom: x =a y, natural_number: $n, token: "$token"
Definitions occuring in definition : ifthenelse: if b then t else f fi , eq_atom: x =a y, token: "$token", natural_number: $n
FDL editor aliases : str1-to-nat

Latex:
str1-to-nat(a) == if a =a "1" then 1 if a =a "2" then 2 if a =a "3" then 3 if a =a "4" then 4 if a =a "5" then 5 if a =a "6" then 6 if a =a "7" then 7 if a =a "8" then 8 if a =a "9" then 9 else 0 fi Date html generated: 2016_05_14-PM-03_35_27 Last ObjectModification: 2015_09_22-PM-06_01_11 Theory : decidable!equality Home Index