/usr/share/maude/term-order.maude is in maude 2.7-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 | ***(
This file is part of the Maude 2 interpreter.
Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA.
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
)
***
*** Strict total ordering on terms of a given kind.
*** Version 2.3.
***
fmod TERM-ORDER{X :: TRIV} is
protecting EXT-BOOL .
protecting CONVERSION .
protecting META-LEVEL .
vars E F : [X$Elt] .
vars Q P : Qid .
vars A B : NeTermList .
vars C D : TermList .
vars T U : Term .
op lt : [X$Elt] [X$Elt] -> Bool .
eq lt(E, F) = $lt(upTerm(E), upTerm(F)) .
op $lt : TermList TermList -> Bool .
eq $lt(Q, P) = string(Q) < string(P) .
eq $lt(Q[A], P) = $lt(Q, P) .
eq $lt(Q, P[B]) = $lt(Q, P) or-else Q == P .
eq $lt(Q[A], P[B]) =
if Q == P then $lt(A, B)
else $lt(Q, P)
fi .
eq $lt(empty, B) = true .
eq $lt(C, empty) = false .
eq $lt((T, C), (U, D)) =
if T == U then $lt(C, D)
else $lt(T, U)
fi .
endfm
|