		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-expr-ops

Gather all of the operators used throughout an expression.

Signature
(vl-expr-ops x) → ops
Arguments: x — Guard (vl-expr-p x).
Returns: ops — Type (vl-oplist-p ops).

We simply gather all of the unary and binary operators used in the expression, with repetition.

Theorem: return-type-of-vl-expr-ops.ops

(defthm return-type-of-vl-expr-ops.ops
  (b* ((?ops (vl-expr-ops x)))
    (vl-oplist-p ops))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-ops.ops

(defthm return-type-of-vl-exprlist-ops.ops
  (b* ((?ops (vl-exprlist-ops x)))
    (vl-oplist-p ops))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-expr-ops

(defthm true-listp-of-vl-expr-ops
  (true-listp (vl-expr-ops x))
  :rule-classes :type-prescription)

Theorem: true-listp-of-vl-exprlist-ops

(defthm true-listp-of-vl-exprlist-ops
  (true-listp (vl-exprlist-ops x))
  :rule-classes :type-prescription)

Theorem: vl-expr-ops-nrev-removal

(defthm vl-expr-ops-nrev-removal
  (equal (vl-expr-ops-nrev x nrev)
         (append nrev (vl-expr-ops x))))

Theorem: vl-exprlist-ops-nrev-removal

(defthm vl-exprlist-ops-nrev-removal
  (equal (vl-exprlist-ops-nrev x nrev)
         (append nrev (vl-exprlist-ops x))))

Theorem: vl-expr-ops-of-vl-expr-fix-x

(defthm vl-expr-ops-of-vl-expr-fix-x
  (equal (vl-expr-ops (vl-expr-fix x))
         (vl-expr-ops x)))

Theorem: vl-exprlist-ops-of-vl-exprlist-fix-x

(defthm vl-exprlist-ops-of-vl-exprlist-fix-x
  (equal (vl-exprlist-ops (vl-exprlist-fix x))
         (vl-exprlist-ops x)))

Theorem: vl-expr-ops-vl-expr-equiv-congruence-on-x

(defthm vl-expr-ops-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr-ops x)
                  (vl-expr-ops x-equiv)))
  :rule-classes :congruence)

Theorem: vl-exprlist-ops-vl-exprlist-equiv-congruence-on-x

(defthm vl-exprlist-ops-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-exprlist-ops x)
                  (vl-exprlist-ops x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-expr-ops-nrev
Vl-exprlist-ops