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.

syntax

(in-package "ACL2")

Required at the start of an ACL2 book. See include-book for more details.

syntax

(set-compile-fns flg)

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

syntax

(set-ignore-ok flg)

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.

syntax

(set-state-ok x)

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

Examples:

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