File: ACL2-PC_colon__colon_WRAP1.html

package info (click to toggle)
acl2 3.1-1
  • links: PTS
  • area: main
  • in suites: etch, etch-m68k
  • size: 36,712 kB
  • ctags: 38,396
  • sloc: lisp: 464,023; makefile: 5,470; sh: 86; csh: 47; cpp: 25; ansic: 22
file content (41 lines) | stat: -rw-r--r-- 1,810 bytes parent folder | download
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
<html>
<head><title>ACL2-PC_colon__colon_WRAP1.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>ACL2-PC::WRAP1</h3>(primitive)
<code>   </code>combine goals into a single goal
<pre>Major Section:  <a href="PROOF-CHECKER-COMMANDS.html">PROOF-CHECKER-COMMANDS</a>
</pre><p>


<pre>
Examples:
; Keep (main . 1) and (main . 2) if they exist, as well as the current goal;
; and for each other goal, conjoin it into the current goal and delete it:
(wrap1 ((main . 1) (main . 2)))<p>

; As explained below, conjoin all subsequent siblings of the current goal
; into the current goal, and then delete them:
(wrap1)
<p>
General Form:
(wrap1 &amp;optional kept-goal-names)
</pre>

If <code>kept-goal-names</code> is not <code>nil</code>, the current goal is replaced by
conjoining it with all goals other than the current goal and those indicated
by <code>kept-goal-names</code>, and those other goals are deleted.  If
<code>kept-goal-names</code> is omitted, then the the current goal must be of the form
<code>(name . n)</code>, and the goals to conjoin into the current goal (and delete)
are those with names of the form <code>(name . k)</code> for <code>k</code> &gt;= <code>n</code>.<p>

NOTE: <code>Wrap1</code> always ``succeeds'', even if there are no other goals to
conjoin into the current goal (a message is printed in that case), and it
always leaves you with no hypotheses at the top of the current goal's
conclusion (as though <code>top</code> and <code>demote</code> had been executed, if
necessary).<p>

Also see proof-checker documentation for <code>wrap</code>
(see <a href="PROOF-CHECKER-COMMANDS.html">proof-checker-commands</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>