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
|
<html>
<head><title>ACL2-PC_colon__colon_PROMOTE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::PROMOTE</h3>(primitive)
<code> </code>move antecedents of conclusion's <code>implies</code> term to top-level
<code> </code>hypotheses
<pre>Major Section: <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>
<pre>
Examples:
promote
(promote t)
</pre>
For example, if the conclusion is <code>(implies (and x y) z)</code>, then
after execution of <code>promote</code>, the conclusion will be <code>z</code> and the terms <code>x</code>
and <code>y</code> will be new top-level hypotheses.
<p>
<pre>
General Form:
(promote &optional do-not-flatten-flag)
</pre>
Replace conclusion of <code>(implies hyps exp)</code> or <code>(if hyps exp t)</code> with
simply <code>exp</code>, adding <code>hyps</code> to the list of top-level hypotheses.
Moreover, if <code>hyps</code> is viewed as a conjunction then each conjunct will
be added as a separate top-level hypothesis. An exception is that
if <code>do-not-flatten-flag</code> is supplied and not <code>nil</code>, then only one
top-level hypothesis will be added, namely <code>hyps</code>.<p>
<strong>Note</strong>: You must be at the top of the conclusion in order to use this
command. Otherwise, first invoke <code>top</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>
|
