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
|
<html>
<head><title>ACTIVE-RUNEP.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ACTIVE-RUNEP</h2>check that a <a href="RUNE.html">rune</a> exists and is <a href="ENABLE.html">enable</a>d
<pre>Major Section: <a href="THEORIES.html">THEORIES</a>
</pre><p>
<pre>
Example:
(active-runep '(:rewrite left-to-right))
<p>
General Form:
(active-runep rune)
</pre>
where <code>rune</code> has the shape of a <a href="RUNE.html">rune</a>. This macro expands to an
expression using the variables <code>ens</code> and <code>state</code>, and returns non-<code>nil</code>
when the given rune exists and is <a href="ENABLE.html">enable</a>d (according to the given
``enabled structure,'' <code>ens</code>, and the current logical <a href="WORLD.html">world</a> of the
given <code><a href="STATE.html">state</a></code>). See <a href="THEORY-INVARIANT.html">theory-invariant</a> for how this macro can be of
use.
<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>
|
