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
|
<html>
<head><title>PCB.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>PCB</h2>print the <a href="COMMAND.html">command</a> block described by a <a href="COMMAND.html">command</a> descriptor
<pre>Major Section: <a href="HISTORY.html">HISTORY</a>
</pre><p>
<pre>
Examples:
:pcb :max ; print the most recent command block
:pcb :x ; print the most recent command block
:pcb fn ; print the command block that introduced fn
:pcb 5 ; print the fifth command block
</pre>
See <a href="COMMAND-DESCRIPTOR.html">command-descriptor</a>.
<p>
<code>Pcb</code> takes one argument, a <a href="COMMAND.html">command</a> descriptor, and prints the <a href="COMMAND.html">command</a>
block of the <a href="COMMAND.html">command</a> described. See <a href="COMMAND-DESCRIPTOR.html">command-descriptor</a> for
details of <a href="COMMAND.html">command</a> descriptors. See <a href="PC.html">pc</a> for description of the
format in which <a href="COMMAND.html">command</a>s are displayed. The <a href="COMMAND.html">command</a> block of a
<a href="COMMAND.html">command</a> consists of the <a href="COMMAND.html">command</a> itself and all of the <a href="EVENTS.html">events</a> it
created. If the <a href="COMMAND.html">command</a> created a single event and that event is in
fact the <a href="COMMAND.html">command</a> (i.e., if the <a href="COMMAND.html">command</a> typed was just an event such
as a <code><a href="DEFUN.html">defun</a></code> or <code><a href="DEFTHM.html">defthm</a></code> rather than a macro that expanded to some event
forms), then <code>pcb</code> just prints the <a href="COMMAND.html">command</a>. <code>Pcb</code> sketches <a href="COMMAND.html">command</a> and
all of the <a href="EVENTS.html">events</a> it created, rather than printing them fully. If
you wish to see just the <a href="COMMAND.html">command</a>, in its entirety, use <code><a href="PC.html">pc</a></code>. If you
wish to see one of the <a href="EVENTS.html">events</a> within the block, in its entirety, use
<code><a href="PE.html">pe</a></code>. If you wish to see the <a href="COMMAND.html">command</a> sketched and all of the <a href="EVENTS.html">events</a>
it created, in their entirety, use <code><a href="PCB_bang_.html">pcb!</a></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>
|
