(vl-choose-parse-error pos1 err1 pos2 err2) → (mv best-pos best-err)
Function:
(defun vl-choose-parse-error (pos1 err1 pos2 err2) (declare (xargs :guard (and (natp pos1) (vl-warning-p err1) (natp pos2) (vl-warning-p err2)))) (let ((__function__ 'vl-choose-parse-error)) (declare (ignorable __function__)) (if (<= (lnfix pos1) (lnfix pos2)) (mv (lnfix pos1) (vl-warning-fix err1)) (mv (lnfix pos2) (vl-warning-fix err2)))))
Theorem:
(defthm natp-of-vl-choose-parse-error.best-pos (b* (((mv ?best-pos ?best-err) (vl-choose-parse-error pos1 err1 pos2 err2))) (natp best-pos)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warning-p-of-vl-choose-parse-error.best-err (b* (((mv ?best-pos ?best-err) (vl-choose-parse-error pos1 err1 pos2 err2))) (vl-warning-p best-err)) :rule-classes :rewrite)
Theorem:
(defthm vl-choose-parse-error-under-iff (b* (((mv ?best-pos ?best-err) (vl-choose-parse-error pos1 err1 pos2 err2))) best-err))