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
|
<html>
<head><title>DEFAULT-DEFUN-MODE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>DEFAULT-DEFUN-MODE</h2>the default <a href="DEFUN-MODE.html">defun-mode</a> of <code><a href="DEFUN.html">defun</a></code>'d functions
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
When a <code><a href="DEFUN.html">defun</a></code> is processed and no <code>:mode</code> <code>xarg</code> is supplied, the
function <code>default-defun-mode</code> is used. To find the default <a href="DEFUN-MODE.html">defun-mode</a>
of the current ACL2 <a href="WORLD.html">world</a>, type <code>(default-defun-mode (w state))</code>.
See <a href="DEFUN-MODE.html">defun-mode</a> for a discussion of <a href="DEFUN-MODE.html">defun-mode</a>s. To change the
default <a href="DEFUN-MODE.html">defun-mode</a> of the ACL2 <a href="WORLD.html">world</a>, type one of the keywords
<code>:</code><code><a href="PROGRAM.html">program</a></code> or <code>:</code><code><a href="LOGIC.html">logic</a></code>.
<p>
The default ACL2 <a href="PROMPT.html">prompt</a> displays the current default <a href="DEFUN-MODE.html">defun-mode</a> by
showing the character <code>p</code> for <code>:</code><code><a href="PROGRAM.html">program</a></code> mode, and omitting it for
<code>:</code><code><a href="LOGIC.html">logic</a></code> mode; see <a href="DEFAULT-PRINT-PROMPT.html">default-print-prompt</a>. The default <a href="DEFUN-MODE.html">defun-mode</a>
may be changed using the keyword <a href="COMMAND.html">command</a>s <code>:</code><code><a href="PROGRAM.html">program</a></code> and <code>:</code><code><a href="LOGIC.html">logic</a></code>,
which are equivalent to the <a href="COMMAND.html">command</a>s <code>(program)</code> and <code>(logic)</code>.
Each of these names is documented separately: see <a href="PROGRAM.html">program</a> and
see <a href="LOGIC.html">logic</a>. The default <a href="DEFUN-MODE.html">defun-mode</a> is stored in the <a href="TABLE.html">table</a>
<code><a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a></code> and hence may also be changed by a <code><a href="TABLE.html">table</a></code>
<a href="COMMAND.html">command</a>. See <a href="TABLE.html">table</a> and also see <a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a>.
Both mode-changing <a href="COMMAND.html">command</a>s are <a href="EVENTS.html">events</a>.<p>
While <a href="EVENTS.html">events</a> that change the default <a href="DEFUN-MODE.html">defun-mode</a> are permitted within
an <code><a href="ENCAPSULATE.html">encapsulate</a></code> or the text of a book, their effects are <code><a href="LOCAL.html">local</a></code> in
scope to the duration of the encapsulation or inclusion. For
example, if the default <a href="DEFUN-MODE.html">defun-mode</a> is <code>:</code><code><a href="LOGIC.html">logic</a></code> and a book is
included that contains the event <code>(program)</code>, then subsequent
<a href="EVENTS.html">events</a> within the book are processed with the default <a href="DEFUN-MODE.html">defun-mode</a>
<code>:</code><code><a href="PROGRAM.html">program</a></code>; but when the <code><a href="INCLUDE-BOOK.html">include-book</a></code> event completes, the
default <a href="DEFUN-MODE.html">defun-mode</a> will still be <code>:</code><code><a href="LOGIC.html">logic</a></code>. <a href="COMMAND.html">Command</a>s that change
the default <a href="DEFUN-MODE.html">defun-mode</a> are not permitted inside <code><a href="LOCAL.html">local</a></code> forms.
<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>
|
