		Search-engine friendly clone of the ACL2 documentation.

Guard

Restricting the domain of a function

NOTE: Novices are often best served by avoiding guards.

The ACL2 system provides a mechanism for restricting a function to a particular domain. Such restrictions are called ``guards.'' A definition's guard has no effect on the logical axiom added when that definition is accepted by ACL2. Moreover, the guard has NO EFFECT on the proof that a recursive definition is admissible — informally, that it terminates). (See mbt for a discussion of one way to use the guard explicitly to assist with that proof while avoiding execution overhead.)

Guards can be useful as a specification device or for increasing execution efficiency. To make such a restriction, use the :guard keyword (see xargs) or, especially if you want the host Lisp compiler to use this information, use type declarations (see declare; also see xargs for a discussion of the :split-types keyword). The general issue of guards and guard verification is discussed in the topics listed below.

To begin further discussion of guards, see guard-introduction. That section directs the reader to further sections for more details. To see just a summary of some commands related to guards, see guard-quick-reference. For a discussion of the use of proof to verify the absence of guard violations, see verify-guards.

Subtopics

Verify-guards: Verify the guards of a function
Mbe: Attach code for execution
Set-guard-checking: Control checking guards during execution of top-level forms
Ec-call: Execute a call in the ACL2 logic instead of raw Lisp
Print-gv: Print a form whose evaluation caused a guard violation
The: Special form for execution efficiency or run-time type checks
Guards-and-evaluation: The relationship between guards and evaluation
Guard-debug: Generate markers to indicate sources of guard proof obligations
Set-check-invariant-risk: Affect certain program-mode updates to stobjs or arrays
Guard-evaluation-table: A table that shows combinations of defun-modes and guard-checking
Guard-evaluation-examples-log: Log showing combinations of defun-modes and guard-checking
Guard-example: A brief transcript illustrating guards in ACL2
Defthmg: Variant of defthm supporting guard verification
Invariant-risk: Potential slowdown for program-mode updates to stobjs or arrays
With-guard-checking: Suppress or enable guard-checking for a form
Guard-miscellany: Miscellaneous remarks about guards
Guard-holders: Remove trivial calls from a term
Guard-formula-utilities: Utilities that show guard proof obligations
Set-verify-guards-eagerness: The eagerness with which guard verification is tried.
Guard-quick-reference: Brief summary of guard checking and guard verification
Set-register-invariant-risk: Avoid invariant-risk checking for specified functions
Guards-for-specification: Guards as a specification device
Guard-evaluation-examples-script: A script to show combinations of defun-modes and guard-checking
Guard-introduction: Introduction to guards in ACL2
Program-only: Functions that cannot be in logic mode
Non-exec: Mark code as non-executable
Set-guard-msg: Specify what is printed when a guard is violated
Safe-mode: A mode that avoids guard violations on primitives
Set-print-gv-defaults: Set default keyword values for print-gv
Guard-theorem-example: How to use a previously-proved guard theorem
With-guard-checking-event: Suppress or enable guard-checking for an event form
With-guard-checking-error-triple: Suppress or enable guard-checking for a form
Guard-checking-inhibited: Avoiding certain warnings when evaluating ACL2 expressions
Extra-info: Sources of measure or guard proof obligations