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
|
<html>
<head><title>ALPHORDER.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ALPHORDER</h2>total order on atoms
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<code>Alphorder</code> is a non-strict total order, a ``less than or equal,'' on
atoms. By ``non-strict total order'' we mean a function that always
returns <code>t</code> or <code>nil</code> and satisfies the following properties.
<blockquote><p>
o Antisymmetry: <code>XrY & YrX -> X=Y</code><p>
o Transitivity: <code>XrY & YrZ -> XrZ</code><p>
o Trichotomy: <code>XrY v YrX</code><p>
</blockquote>
Also see <a href="LEXORDER.html">lexorder</a>, which extends <code>alphorder</code> to all objects.<p>
<code>(Alphorder x y)</code> has a guard of <code>(and (atom x) (atom y))</code>.
<p>
Within a single type: rationals are compared arithmetically, complex
rationals are compared lexicographically, characters are compared
via their char-codes, and strings and symbols are compared with
alphabetic ordering. Across types, rationals come before complexes,
complexes come before characters, characters before strings, and
strings before symbols. We also allow for ``bad atoms,'' i.e.,
atoms that are not legal Lisp objects but make sense in the ACL2
logic; these come at the end, after symbols.
<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>
|
