! relation.txt - utility predicates for ordering & [in]equality predicates !/ (bit ) - set of bit atoms (`0 `1) < - ordering for natural numbers and bits < - lexicographic ordering of sequences of number & bit expressions <=, >, >=, /= - other relational operations defined from < = - identical expressions (same as ==) (not_in ) - x is not in a sequence (given /=) (different ) - all elements in sequence are pair-wise unequal (different- ) - all different elements in seq are from named set !\ ! ? Should we define lexicographic ordering (< ) on set elements? ! " other relations (<= ), (> ), ... too? ! bit - set of bit atoms (finite_set bit (`0 `1)). ! -- this defines ord and < on bit atoms ! < - top-level ordering relation applies to natural numbers or bits (< %1 %2)< (one_valid ((< num) %1 %2) ((< bit) %1 %2)). ! -- note that natural number and bit types are distinct ! < - lexicographic ordering of expressions with natural numbers and bits (< (\$) (\$ % \$x)). (< (\$ %1 \$1) (\$ %2 \$2))< (< %1 %2). ! From bit ordering we get ordering of characters, char strings, and symbols. ! <=, >, >=, /= - other ordering relations (<= % %). (<= %1 %2)< (< %1 %2). (> %1 %2)< (< %2 %1). (>= %1 %2)< (<= %2 %1). (/= %1 %2)< (one_valid (< %1 %2) (> %1 %2)). ! This gives inequality between distinct characters, character strings, ! and symbols, as well as different natural numbers. ! = - equal (identical) expressions ! (Might be nice to limit this to just natural number & bit expressions?) (= % %). ! not_in - (not_member) - element is not in a sequence (given /= relation) ! -- This is only defined where the inequality relation /= holds. (not_in %x %seq)< (1* /= %x %seq). ! different - all elements in sequence are pair-wise unequal (/=) (different %seq)< (binrel* /= %seq). ! different- - all different elements in sequence are from the named set ! - set must have inequality relation defined (different- %set %seq)< (all %set %seq), (different %seq).