		Search-engine friendly clone of the ACL2 documentation.

Svex-alist

Svex-acons

Like acons, but with proper fty-discipline for svex-alists.

Signature
(svex-acons var v a) → aa
Arguments: var — Guard (svar-p var).; v — Guard (svex-p v).; a — Guard (svex-alist-p a).
Returns: aa — Type (svex-alist-p aa).

Definitions and Theorems

Function: svex-acons

(defun svex-acons (var v a)
  (declare (xargs :guard (and (svar-p var)
                              (svex-p v)
                              (svex-alist-p a))))
  (let ((__function__ 'svex-acons))
    (declare (ignorable __function__))
    (mbe :logic (cons (cons (svar-fix var) (svex-fix v))
                      (svex-alist-fix a))
         :exec (cons (cons var v) a))))

Theorem: svex-alist-p-of-svex-acons

(defthm svex-alist-p-of-svex-acons
  (b* ((aa (svex-acons var v a)))
    (svex-alist-p aa))
  :rule-classes :rewrite)

Theorem: svex-acons-of-svar-fix-var

(defthm svex-acons-of-svar-fix-var
  (equal (svex-acons (svar-fix var) v a)
         (svex-acons var v a)))

Theorem: svex-acons-svar-equiv-congruence-on-var

(defthm svex-acons-svar-equiv-congruence-on-var
  (implies (svar-equiv var var-equiv)
           (equal (svex-acons var v a)
                  (svex-acons var-equiv v a)))
  :rule-classes :congruence)

Theorem: svex-acons-of-svex-fix-v

(defthm svex-acons-of-svex-fix-v
  (equal (svex-acons var (svex-fix v) a)
         (svex-acons var v a)))

Theorem: svex-acons-svex-equiv-congruence-on-v

(defthm svex-acons-svex-equiv-congruence-on-v
  (implies (svex-equiv v v-equiv)
           (equal (svex-acons var v a)
                  (svex-acons var v-equiv a)))
  :rule-classes :congruence)

Theorem: svex-acons-of-svex-alist-fix-a

(defthm svex-acons-of-svex-alist-fix-a
  (equal (svex-acons var v (svex-alist-fix a))
         (svex-acons var v a)))

Theorem: svex-acons-svex-alist-equiv-congruence-on-a

(defthm svex-acons-svex-alist-equiv-congruence-on-a
  (implies (svex-alist-equiv a a-equiv)
           (equal (svex-acons var v a)
                  (svex-acons var v a-equiv)))
  :rule-classes :congruence)