		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Expr-grade-index

Signature
(expr-grade-index grade) → index
Arguments: grade — Guard (expr-gradep grade).
Returns: index — Type (natp index).

Definitions and Theorems

Function: expr-grade-index

(defun expr-grade-index (grade)
  (declare (xargs :guard (expr-gradep grade)))
  (let ((__function__ 'expr-grade-index))
    (declare (ignorable __function__))
    (expr-grade-case grade
                     :top 14
                     :conditional 14
                     :disjunctive 13
                     :conjunctive 12
                     :equality 11
                     :ordering 10
                     :bitwise-xor 9
                     :bitwise-ior 8
                     :bitwise-and 7
                     :shift 6
                     :additive 5
                     :multiplicative 4
                     :exponential 3
                     :unary 2
                     :postfix 1
                     :primary 0)))

Theorem: natp-of-expr-grade-index

(defthm natp-of-expr-grade-index
  (b* ((index (expr-grade-index grade)))
    (natp index))
  :rule-classes :rewrite)

Theorem: expr-grade-index-of-expr-grade-fix-grade

(defthm expr-grade-index-of-expr-grade-fix-grade
  (equal (expr-grade-index (expr-grade-fix grade))
         (expr-grade-index grade)))

Theorem: expr-grade-index-expr-grade-equiv-congruence-on-grade

(defthm expr-grade-index-expr-grade-equiv-congruence-on-grade
  (implies (expr-grade-equiv grade grade-equiv)
           (equal (expr-grade-index grade)
                  (expr-grade-index grade-equiv)))
  :rule-classes :congruence)