		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-priority->=

Total order on expression priorities: greater than or equal to.

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))))
  (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)