		Search-engine friendly clone of the ACL2 documentation.

Vl-exprlist

Vl-exprlist-fix

(vl-exprlist-fix x) is a usual fty list fixing function.

Signature
(vl-exprlist-fix x) → fty::newx
Arguments: x — Guard (vl-exprlist-p x).
Returns: fty::newx — Type (vl-exprlist-p fty::newx).

In the logic, we apply vl-expr-fix to each member of the x. In the execution, none of that is actually necessary and this is just an inlined identity function.

Theorem: vl-exprlist-fix-of-list-fix

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

Theorem: vl-exprlist-fix-of-rev

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

Theorem: vl-exprlist-fix-of-nthcdr

(defthm vl-exprlist-fix-of-nthcdr
  (equal (vl-exprlist-fix (nthcdr n x))
         (nthcdr n (vl-exprlist-fix x))))

Theorem: vl-exprlist-fix-of-take

(defthm vl-exprlist-fix-of-take
  (equal (take n (vl-exprlist-fix x))
         (if (<= (nfix n) (len x))
             (vl-exprlist-fix (take n x))
           (append (vl-exprlist-fix x)
                   (replicate (- (nfix n) (len x)) nil)))))

Theorem: vl-exprlist-equiv-implies-vl-exprlist-equiv-list-fix-1

(defthm vl-exprlist-equiv-implies-vl-exprlist-equiv-list-fix-1
  (implies (vl-exprlist-equiv x x-equiv)
           (vl-exprlist-equiv (list-fix x)
                              (list-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: vl-exprlist-equiv-implies-vl-exprlist-equiv-rev-1

(defthm vl-exprlist-equiv-implies-vl-exprlist-equiv-rev-1
  (implies (vl-exprlist-equiv x x-equiv)
           (vl-exprlist-equiv (rev x)
                              (rev x-equiv)))
  :rule-classes (:congruence))