1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
<html>
<head><title>GUARD.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>GUARD</h2>restricting the domain of a function
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
The ACL2 system provides a mechanism for restricting a function
definition to a particular domain. Although such restrictions,
which are called ``guards,'' are actually ignored by the ACL2
<em>logic</em>, they can be useful as a specification device or as a
means of causing the execution of definitions directly in Common
Lisp. To make such a restriction, use the <code>:guard</code> <code>xarg</code> to
<code><a href="DEFUN.html">defun</a></code>. See <a href="XARGS.html">xargs</a> for a discussion of how to use <code>:guard</code>.
The general issue of guards and guard verification is discussed
in the topics listed below.
<p>
<ul>
<li><h3><a href="GUARD-EVALUATION-EXAMPLES-LOG.html">GUARD-EVALUATION-EXAMPLES-LOG</a> -- log showing combinations of <a href="DEFUN-MODE.html">defun-mode</a>s and <a href="GUARD.html">guard</a>-checking
</h3>
</li>
<li><h3><a href="GUARD-EVALUATION-EXAMPLES-SCRIPT.html">GUARD-EVALUATION-EXAMPLES-SCRIPT</a> -- a script to show combinations of <a href="DEFUN-MODE.html">defun-mode</a>s and <a href="GUARD.html">guard</a>-checking
</h3>
</li>
<li><h3><a href="GUARD-EVALUATION-TABLE.html">GUARD-EVALUATION-TABLE</a> -- a table that shows combinations of <a href="DEFUN-MODE.html">defun-mode</a>s and <a href="GUARD.html">guard</a>-checking
</h3>
</li>
<li><h3><a href="GUARD-EXAMPLE.html">GUARD-EXAMPLE</a> -- a brief transcript illustrating <a href="GUARD.html">guard</a>s in ACL2
</h3>
</li>
<li><h3><a href="GUARD-INTRODUCTION.html">GUARD-INTRODUCTION</a> -- introduction to <a href="GUARD.html">guard</a>s in ACL2
</h3>
</li>
<li><h3><a href="GUARD-MISCELLANY.html">GUARD-MISCELLANY</a> -- miscellaneous remarks about guards
</h3>
</li>
<li><h3><a href="GUARD-QUICK-REFERENCE.html">GUARD-QUICK-REFERENCE</a> -- brief summary of guard checking and guard verification
</h3>
</li>
<li><h3><a href="GUARDS-AND-EVALUATION.html">GUARDS-AND-EVALUATION</a> -- the relationship between guards and evaluation
</h3>
</li>
<li><h3><a href="GUARDS-FOR-SPECIFICATION.html">GUARDS-FOR-SPECIFICATION</a> -- guards as a specification device
</h3>
</li>
<li><h3><a href="SET-GUARD-CHECKING.html">SET-GUARD-CHECKING</a> -- control checking <a href="GUARD.html">guard</a>s during execution of top-level forms
</h3>
</li>
<li><h3><a href="SET-VERIFY-GUARDS-EAGERNESS.html">SET-VERIFY-GUARDS-EAGERNESS</a> -- the eagerness with which <a href="GUARD.html">guard</a> verification is tried.
</h3>
</li>
<li><h3><a href="VERIFY-GUARDS.html">VERIFY-GUARDS</a> -- verify the <a href="GUARD.html">guard</a>s of a function
</h3>
</li>
</ul>
To begin further discussion of guards, see <a href="GUARD-INTRODUCTION.html">guard-introduction</a>.
That section directs the reader to further sections for more
details. To see just a summary of some <a href="COMMAND.html">command</a>s related to guards,
see <a href="GUARD-QUICK-REFERENCE.html">guard-quick-reference</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
