		Search-engine friendly clone of the ACL2 documentation.

Vl-warning-sort

Vl-warning-<

A basic, rather arbitrary ordering for warnings.

Signature
(vl-warning-< x y) → *
Arguments: x — Guard (vl-warning-p x).; y — Guard (vl-warning-p y).

Definitions and Theorems

Function: vl-warning-<

(defun vl-warning-< (x y)
  (declare (xargs :guard (and (vl-warning-p x)
                              (vl-warning-p y))))
  (let ((__function__ 'vl-warning-<))
    (declare (ignorable __function__))
    (b* (((vl-warning x) x)
         ((vl-warning y) y)
         ((when (symbol< x.type y.type)) t)
         ((unless (eq x.type y.type)) nil)
         ((when (<< x.fn y.fn)) t)
         ((unless (eq x.fn y.fn)) nil)
         ((when (string< x.msg y.msg)) t)
         ((unless (equal x.msg y.msg)) nil)
         ((when (<< x.args y.args)) t)
         ((unless (equal x.args y.args)) nil))
      (<< x.fatalp y.fatalp))))

Theorem: vl-warning-<-transitive

(defthm vl-warning-<-transitive
  (implies (and (vl-warning-< x y)
                (vl-warning-< y z))
           (vl-warning-< x z)))

Theorem: vl-warning-<-of-vl-warning-fix-x

(defthm vl-warning-<-of-vl-warning-fix-x
  (equal (vl-warning-< (vl-warning-fix x) y)
         (vl-warning-< x y)))

Theorem: vl-warning-<-vl-warning-equiv-congruence-on-x

(defthm vl-warning-<-vl-warning-equiv-congruence-on-x
  (implies (vl-warning-equiv x x-equiv)
           (equal (vl-warning-< x y)
                  (vl-warning-< x-equiv y)))
  :rule-classes :congruence)

Theorem: vl-warning-<-of-vl-warning-fix-y

(defthm vl-warning-<-of-vl-warning-fix-y
  (equal (vl-warning-< x (vl-warning-fix y))
         (vl-warning-< x y)))

Theorem: vl-warning-<-vl-warning-equiv-congruence-on-y

(defthm vl-warning-<-vl-warning-equiv-congruence-on-y
  (implies (vl-warning-equiv y y-equiv)
           (equal (vl-warning-< x y)
                  (vl-warning-< x y-equiv)))
  :rule-classes :congruence)