		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-patternkey->subexprs

Signature
(vl-patternkey->subexprs x) → subexprs
Arguments: x — Guard (vl-patternkey-p x).
Returns: subexprs — Type (vl-exprlist-p subexprs).

Definitions and Theorems

Function: vl-patternkey->subexprs

(defun vl-patternkey->subexprs (x)
       (declare (xargs :guard (vl-patternkey-p x)))
       (let ((__function__ 'vl-patternkey->subexprs))
            (declare (ignorable __function__))
            (vl-patternkey-case x
                                :expr (list x.key)
                                :otherwise nil)))

Theorem: vl-exprlist-p-of-vl-patternkey->subexprs

(defthm vl-exprlist-p-of-vl-patternkey->subexprs
        (b* ((subexprs (vl-patternkey->subexprs x)))
            (vl-exprlist-p subexprs))
        :rule-classes :rewrite)

Theorem: vl-exprlist-count-of-vl-patternkey->subexprs

(defthm vl-exprlist-count-of-vl-patternkey->subexprs
        (b* ((?subexprs (vl-patternkey->subexprs x)))
            (<= (vl-exprlist-count subexprs)
                (vl-patternkey-count x)))
        :rule-classes :linear)

Theorem: vl-patternkey->subexprs-of-vl-patternkey-fix-x

(defthm vl-patternkey->subexprs-of-vl-patternkey-fix-x
        (equal (vl-patternkey->subexprs (vl-patternkey-fix x))
               (vl-patternkey->subexprs x)))

Theorem: vl-patternkey->subexprs-vl-patternkey-equiv-congruence-on-x

(defthm vl-patternkey->subexprs-vl-patternkey-equiv-congruence-on-x
        (implies (vl-patternkey-equiv x x-equiv)
                 (equal (vl-patternkey->subexprs x)
                        (vl-patternkey->subexprs x-equiv)))
        :rule-classes :congruence)