File: DEFAULT-PRINT-PROMPT.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 (58 lines) | stat: -rw-r--r-- 2,244 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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
 
<html>
<head><title>DEFAULT-PRINT-PROMPT.html  --  ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DEFAULT-PRINT-PROMPT</h2>the default <a href="PROMPT.html">prompt</a> printed by <code><a href="LD.html">ld</a></code>
<pre>Major Section:  <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>


<pre>
Example prompt:
ACL2 p!s&gt;
</pre>

The <a href="PROMPT.html">prompt</a> printed by ACL2 displays the current package, followed by
a space, followed by zero or more of the three <a href="CHARACTERS.html">characters</a> as
specified below, followed by the character <code><a href="_gt_.html">&gt;</a></code> printed one or more
times, reflecting the number of recursive calls of <code><a href="LD.html">ld</a></code>.  The three
<a href="CHARACTERS.html">characters</a> in the middle are as follows:

<pre>
p     ; when (default-defun-mode (w state)) is :program
!     ; when guard checking is on
s     ; when (ld-skip-proofsp state) is t
</pre>

See <a href="DEFAULT-DEFUN-MODE.html">default-defun-mode</a>, see <a href="SET-GUARD-CHECKING.html">set-guard-checking</a>, and
see <a href="LD-SKIP-PROOFSP.html">ld-skip-proofsp</a>.
<p>
Also see <a href="LD-PROMPT.html">ld-prompt</a> to see how to install your own <a href="PROMPT.html">prompt</a>.<p>

Here are some examples with <code>ld-skip-proofsp nil</code>.

<pre>
ACL2 !&gt;    ; logic mode with guard checking on
ACL2 &gt;     ; logic mode with guard checking off
ACL2 p!&gt;   ; program mode with guard checking on
ACL2 p&gt;    ; program mode with guard checking off
</pre>

Here are some examples with <code><a href="DEFAULT-DEFUN-MODE.html">default-defun-mode</a></code> of <code>:</code><code><a href="LOGIC.html">logic</a></code>.

<pre>
ACL2 &gt;     ; guard checking off, ld-skip-proofsp nil
ACL2 s&gt;    ; guard checking off, ld-skip-proofsp t
ACL2 !&gt;    ; guard checking on, ld-skip-proofsp nil
ACL2 !s&gt;   ; guard checking on, ld-skip-proofsp t
</pre>

Finally, here is the prompt in raw mode (see <a href="SET-RAW-MODE.html">set-raw-mode</a>),
regardless of the settings above:

<pre>
ACL2 P&gt;
</pre>

<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>