Modular Arithmetic : Background |
 |
- Cannot simply declare Common Lisp + operator as 32 bits
- The result of adding two 32-bit numbers is 33 bits
- Implies that the guard condition is generally unsatisfiable
- GCL normally recognizes only the symbol "+" as addition
- Cannot provide a logical replacement for + in ACL2
- No efficient implementation of 32-bit addition in ACL2
|
|
|
|