		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Svexlist-unquote

Signature
(svexlist-unquote x) → objs
Arguments: x — Guard (svexlist-p x).
Returns: objs — Type (4veclist-p objs).

Definitions and Theorems

Function: svexlist-unquote

(defun svexlist-unquote (x)
  (declare (xargs :guard (svexlist-p x)))
  (declare (xargs :guard (svexlist-quotesp x)))
  (let ((__function__ 'svexlist-unquote))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom x)
             nil
           (cons (svex-quote->val (car x))
                 (svexlist-unquote (cdr x))))
         :exec x)))

Theorem: 4veclist-p-of-svexlist-unquote

(defthm 4veclist-p-of-svexlist-unquote
  (b* ((objs (svexlist-unquote x)))
    (4veclist-p objs))
  :rule-classes :rewrite)

Theorem: svexlist-unquote-correct

(defthm svexlist-unquote-correct
  (implies (svexlist-quotesp x)
           (equal (svexlist-eval x env)
                  (svexlist-unquote x))))

Theorem: svexlist-unquote-of-svexlist-fix-x

(defthm svexlist-unquote-of-svexlist-fix-x
  (equal (svexlist-unquote (svexlist-fix x))
         (svexlist-unquote x)))

Theorem: svexlist-unquote-svexlist-equiv-congruence-on-x

(defthm svexlist-unquote-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-unquote x)
                  (svexlist-unquote x-equiv)))
  :rule-classes :congruence)