1.5 Theorem Prover Controls
These terms control options for the logic of the ACL2 theorem prover.
| (in-package "ACL2") |
Required at the start of an ACL2 book. See include-book for
more details.
| (set-compile-fns flg) |
If passed t, functions will be compiled as you go along.
Examples: |
| > (set-compile-fns nil) |
| > (set-compile-fns t) |
| (set-ignore-ok flg) |
Examples: |
| > (set-ignore-ok t) |
| > (set-ignore-ok :warn) |
| > (set-ignore-ok nil) |
If passed t, irrelevant formals will be allowed in definitions.
Examples: |
| > (set-irrelevant-formals-ok t) |
| > (set-irrelevant-formals-ok :warn) |
| > (set-irrelevant-formals-ok nil) |
| (set-state-ok x) |
If passed t, STATE will be allowed as a formal parameter.
Examples: |
| > (set-state-ok nil) |
| > (set-state-ok t) |