On this page:
in-package
set-compile-fns
set-ignore-ok
set-irrelevant-formals-ok
set-state-ok

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.

If passed t, functions will be compiled as you go along.

If passed t, unused formals and locals will be allowed without an ignore or ignorable declaration.

Examples:

> (set-ignore-ok t)
> (set-ignore-ok :warn)
> (set-ignore-ok nil)

If passed t, irrelevant formals will be allowed in definitions.

If passed t, STATE will be allowed as a formal parameter.

Examples:

> (set-state-ok nil)
> (set-state-ok t)