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
|
<html>
<head><title>ACL2-PC_colon__colon_HYPS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::HYPS</h3>(macro)
<code> </code>print the hypotheses
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Examples:
hyps -- print all (top-level) hypotheses
(hyps (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4
(hyps (1 3) t) -- print hypotheses 1 and 3 and all governors
<p>
General Form:
(hyps &optional hyps-indices govs-indices)
</pre>
Print the indicated top-level hypotheses and governors. (The notion
of ``governors'' is defined below.) Here, <code>hyps-indices</code> and
<code>govs-indices</code> should be lists of indices of hypotheses and governors
(respectively), except that the atom <code>t</code> may be used to indicate that
one wants all hypotheses or governors (respectively).<p>
The list of ``governors'' is defined as follows. Actually, we
define here the notion of the governors for a pair of the form
<code><term</code>, address>]; we're interested in the special case where the
term is the conclusion and the address is the current address. If
the address is <code>nil</code>, then there are no governors, i.e., the list of
governors is <code>nil</code>. If the term is of the form <code>(if x y z)</code> and the
address is of the form <code>(2 . rest)</code> or <code>(3 . rest)</code>, then the list of
governors is the result of <code>cons</code>ing <code>x</code> or its negation (respectively)
onto the list of governors for the pair <code><y, rest></code> or the pair
<code><z, rest></code> (respectively). If the term is of the form <code>(implies x y)</code>
and the address is of the form <code>(2 . rest)</code>, then the list of
governors is the result of <code>cons</code>ing <code>x</code> onto the list of governors for
the pair <code><y, rest></code>. Otherwise, the list of governors for the pair
<code><term, (n . rest)></code> is exactly the list of governors for the pair
<code><argn, rest></code> where <code>argn</code> is the <code>n</code>th argument of <code>term</code>.<p>
If all goals have been proved, a message saying so will be printed.
(as there will be no current hypotheses or governors!).<p>
The <code>hyps</code> command never causes an error. It ``succeeds'' (in fact
its value is <code>t</code>) if the arguments (when supplied) are appropriate,
i.e. either <code>t</code> or lists of indices of hypotheses or governors,
respectively. Otherwise it ``fails'' (its value is <code>nil</code>).
<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>
|
