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
|
<html>
<head><title>SET-ACL2-PRINT-BASE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>SET-ACL2-PRINT-BASE</h3>control radix in which number are printed
<pre>Major Section: <a href="IO.html">IO</a>
</pre><p>
By default, integers and ratios are printed in base 10. ACL2 also supports
printing in radix 2, 8, or 16 by calling set-acl2-print-base with the desired
radix (base).
<pre>
:set-acl2-print-base 10 ; Default printing
(set-acl2-print-base 10) ; Same as above
:set-acl2-print-base 16 ; Print integers and ratios in hex, e.g., #x3A
(set-acl2-print-base 16) ; Same as above
</pre>
<p>
Note: ACL2 <a href="EVENTS.html">events</a> and some other top-level commands (for example,
<code><a href="THM.html">thm</a></code>, <code><a href="VERIFY.html">verify</a></code>, and history commands such as <code>:</code><code>pe</code> and
<code>:</code><code>pbt</code>) set the print base to 10 during their evaluation. So
<code><a href="SET-ACL2-PRINT-BASE.html">set-acl2-print-base</a></code> has no effect while these forms are being
processed.
<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>
|
