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.

Examples:

  > (set-compile-fns nil)
  > (set-compile-fns t)

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)

  t