		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Sv::svexlist-args-extract-constants

Signature
(sv::svexlist-args-extract-constants acl2::x) → sv::vals
Arguments: acl2::x — Guard (sv::svexlist-p acl2::x).
Returns: sv::vals — Type (sv::maybe-4veclist-p sv::vals).

Definitions and Theorems

Function: svexlist-args-extract-constants

(defun sv::svexlist-args-extract-constants (acl2::x)
  (declare (xargs :guard (sv::svexlist-p acl2::x)))
  (let ((__function__ 'sv::svexlist-args-extract-constants))
    (declare (ignorable __function__))
    (if (atom acl2::x)
        nil
      (cons (b* ((sv::new (sv::svex-reduce-consts (car acl2::x))))
              (sv::svex-case sv::new
                             :quote sv::new.val
                             :otherwise nil))
            (sv::svexlist-args-extract-constants (cdr acl2::x))))))

Theorem: maybe-4veclist-p-of-svexlist-args-extract-constants

(defthm sv::maybe-4veclist-p-of-svexlist-args-extract-constants
  (b* ((sv::vals (sv::svexlist-args-extract-constants acl2::x)))
    (sv::maybe-4veclist-p sv::vals))
  :rule-classes :rewrite)

Theorem: svexlist-args-extract-constants-of-svexlist-fix-x

(defthm sv::svexlist-args-extract-constants-of-svexlist-fix-x
 (equal
    (sv::svexlist-args-extract-constants (sv::svexlist-fix acl2::x))
    (sv::svexlist-args-extract-constants acl2::x)))

Theorem: svexlist-args-extract-constants-svexlist-equiv-congruence-on-x

(defthm
 sv::svexlist-args-extract-constants-svexlist-equiv-congruence-on-x
 (implies (sv::svexlist-equiv acl2::x sv::x-equiv)
          (equal (sv::svexlist-args-extract-constants acl2::x)
                 (sv::svexlist-args-extract-constants sv::x-equiv)))
 :rule-classes :congruence)