		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-priority-<

Total order on expression priorities: less than.

Signature
(expr-priority-< prio1 prio2) → yes/no
Arguments: prio1 — Guard (expr-priorityp prio1).; prio2 — Guard (expr-priorityp prio2).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: expr-priority-<

(defun expr-priority-< (prio1 prio2)
  (declare (xargs :guard (and (expr-priorityp prio1)
                              (expr-priorityp prio2))))
  (not (expr-priority-<= prio2 prio1)))

Theorem: booleanp-of-expr-priority-<

(defthm booleanp-of-expr-priority-<
  (b* ((yes/no (expr-priority-< prio1 prio2)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: expr-priority-<-of-expr-priority-fix-prio1

(defthm expr-priority-<-of-expr-priority-fix-prio1
  (equal (expr-priority-< (expr-priority-fix prio1)
                          prio2)
         (expr-priority-< prio1 prio2)))

Theorem: expr-priority-<-expr-priority-equiv-congruence-on-prio1

(defthm expr-priority-<-expr-priority-equiv-congruence-on-prio1
  (implies (expr-priority-equiv prio1 prio1-equiv)
           (equal (expr-priority-< prio1 prio2)
                  (expr-priority-< prio1-equiv prio2)))
  :rule-classes :congruence)

Theorem: expr-priority-<-of-expr-priority-fix-prio2

(defthm expr-priority-<-of-expr-priority-fix-prio2
  (equal (expr-priority-< prio1 (expr-priority-fix prio2))
         (expr-priority-< prio1 prio2)))

Theorem: expr-priority-<-expr-priority-equiv-congruence-on-prio2

(defthm expr-priority-<-expr-priority-equiv-congruence-on-prio2
  (implies (expr-priority-equiv prio2 prio2-equiv)
           (equal (expr-priority-< prio1 prio2)
                  (expr-priority-< prio1 prio2-equiv)))
  :rule-classes :congruence)