2.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 Books and Teachpacks 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)

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)

(set-irrelevant-formals-ok flg)

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)

t