		Search-engine friendly clone of the ACL2 documentation.

Ctxexprs

Vl-taskdecl-ctxexprs

Signature
(vl-taskdecl-ctxexprs mod x) → alist
Arguments: mod — Guard (stringp mod).; x — Guard (vl-taskdecl-p x).
Returns: alist — Type (vl-exprctxalist-p alist).

Definitions and Theorems

Function: vl-taskdecl-ctxexprs

(defun vl-taskdecl-ctxexprs (mod x)
  (declare (xargs :guard (and (stringp mod) (vl-taskdecl-p x))))
  (let ((__function__ 'vl-taskdecl-ctxexprs))
    (declare (ignorable __function__))
    (let ((x (vl-taskdecl-fix x)))
      (vl-make-exprctxalist (vl-taskdecl-allexprs x)
                            (make-vl-context1 :mod mod :elem x)))))

Theorem: vl-exprctxalist-p-of-vl-taskdecl-ctxexprs

(defthm vl-exprctxalist-p-of-vl-taskdecl-ctxexprs
  (b* ((alist (vl-taskdecl-ctxexprs mod x)))
    (vl-exprctxalist-p alist))
  :rule-classes :rewrite)

Theorem: vl-taskdecl-ctxexprs-of-str-fix-mod

(defthm vl-taskdecl-ctxexprs-of-str-fix-mod
  (equal (vl-taskdecl-ctxexprs (str-fix mod) x)
         (vl-taskdecl-ctxexprs mod x)))

Theorem: vl-taskdecl-ctxexprs-streqv-congruence-on-mod

(defthm vl-taskdecl-ctxexprs-streqv-congruence-on-mod
  (implies (streqv mod mod-equiv)
           (equal (vl-taskdecl-ctxexprs mod x)
                  (vl-taskdecl-ctxexprs mod-equiv x)))
  :rule-classes :congruence)

Theorem: vl-taskdecl-ctxexprs-of-vl-taskdecl-fix-x

(defthm vl-taskdecl-ctxexprs-of-vl-taskdecl-fix-x
  (equal (vl-taskdecl-ctxexprs mod (vl-taskdecl-fix x))
         (vl-taskdecl-ctxexprs mod x)))

Theorem: vl-taskdecl-ctxexprs-vl-taskdecl-equiv-congruence-on-x

(defthm vl-taskdecl-ctxexprs-vl-taskdecl-equiv-congruence-on-x
  (implies (vl-taskdecl-equiv x x-equiv)
           (equal (vl-taskdecl-ctxexprs mod x)
                  (vl-taskdecl-ctxexprs mod x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-taskdecl-ctxexprs-nrev