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

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