Recursion and Induction: Numbers

The only numbers we will use are the integers, written in the usual way,
e.g., `-3`, `0`, and `123`.
ACL2 allows integers to be written in other ways, e.g., `00123`,
`+123`, `246/2`, `#b1111011`, `#o173` and `#x7B` are
all ways to write `123`. However, we will always write them in
conventional decimal notation.

ACL2 also supports rationals, e.g., `1/3` and `22/7`, and complex
rationals, e.g., `#c(5 2)`, which is more commonly written 5 + 2*i*. Lisp, but
not ACL2, supports floating point numbers, e.g., `3.1415` and
`31415E-4`.

(Maybe explore <<numbers>>?)

Next: