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>SET-ACL2-PRINT-CASE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>SET-ACL2-PRINT-CASE</h3>control whether symbols are printed in upper case or in lower case
<pre>Major Section: <a href="IO.html">IO</a>
</pre><p>
By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp. As with Common Lisp,
ACL2 supports printing in a "downcase" mode, where symbols are
printed in lower case. Many printing functions (some details below)
print characters in lower case for a symbol when the ACL2 <a href="STATE.html">state</a>
global variable <code>print-case</code> has value <code>:downcase</code> and vertical bars
are not necessary for printing that symbol. (Thus, this state global
functions in complete analogy to the Common Lisp global
<code>*print-case*</code>.) The value <code>print-case</code> is returned by
<code>(acl2-print-case)</code>, and may be set using the macro
<code>set-acl2-print-case</code> (which returns <code><a href="STATE.html">state</a></code>), as follows.
<pre>
:set-acl2-print-case :upcase ; Default printing
(set-acl2-print-case :upcase) ; Same as above
:set-acl2-print-case :downcase ; Print symbols in lower case when
; vertical bars are not required
(set-acl2-print-case :downcase) ; Same as above
</pre>
The ACL2 user can expect that the <code>:downcase</code> setting will have an
effect for formatted output (see <a href="FMT.html">fmt</a> and see <a href="FMS.html">fms</a>) when the
directives are <code>~p</code>, <code>~P</code>, <code>~q</code>, or <code>~Q</code>, for built-in functions <code>princ$</code> and
<code>prin1$</code>, and the <code>ppr</code> family of functions, and <em>not</em> for built-in
function <code>print-object$</code>. For other printing functions, the effect of
<code>:downcase</code> is unspecified.
<p>
<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>
|
