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 + 2i. Lisp, but not ACL2, supports floating point numbers, e.g., 3.1415 and 31415E-4.
(Maybe explore <<numbers>>?)