1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
<html>
<head><title>LEXORDER.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>LEXORDER</h2>total order on ACL2 objects
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<code>Lexorder</code> is a non-strict total order, a ``less than or equal,'' on
ACL2 objects. Also see <a href="ALPHORDER.html">alphorder</a>, the restriction of <code>lexorder</code> to
atoms; the notion of ``non-strict total order'' is defined there.<p>
<code>Lexorder</code> has a guard of <code>t</code>.
<p>
For <code>lexorder</code>, an <a href="ATOM.html">atom</a> and a <a href="CONS.html">cons</a> are ordered so that
the <a href="ATOM.html">atom</a> comes first, and two <a href="CONS.html">cons</a>es are ordered so that
the one with the recursively smaller <code><a href="CAR.html">car</a></code> comes first, with the
<code><a href="CDR.html">cdr</a></code>s being compared only if the <code><a href="CAR.html">car</a></code>s are equal. <code>Lexorder</code>
compares two atoms by using <code><a href="ALPHORDER.html">alphorder</a></code>.
<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>
|
