		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Update-elab-mod$a->name

Signature
(update-elab-mod$a->name name elab-mod$a) → elab-mod$a2
Arguments: name — Guard (modname-p name).; elab-mod$a — Guard (elab-mod$ap elab-mod$a).
Returns: elab-mod$a2 — Type (elab-mod$ap elab-mod$a2).

Definitions and Theorems

Function: update-elab-mod$a->name

(defun update-elab-mod$a->name (name elab-mod$a)
  (declare (xargs :guard (and (modname-p name)
                              (elab-mod$ap elab-mod$a))))
  (let ((__function__ 'update-elab-mod$a->name))
    (declare (ignorable __function__))
    (s :name (modname-fix name)
       (elab-mod$a-fix elab-mod$a))))

Theorem: elab-mod$ap-of-update-elab-mod$a->name

(defthm elab-mod$ap-of-update-elab-mod$a->name
  (b* ((elab-mod$a2 (update-elab-mod$a->name name elab-mod$a)))
    (elab-mod$ap elab-mod$a2))
  :rule-classes :rewrite)

Theorem: update-elab-mod$a->name-of-modname-fix-name

(defthm update-elab-mod$a->name-of-modname-fix-name
  (equal (update-elab-mod$a->name (modname-fix name)
                                  elab-mod$a)
         (update-elab-mod$a->name name elab-mod$a)))

Theorem: update-elab-mod$a->name-modname-equiv-congruence-on-name

(defthm update-elab-mod$a->name-modname-equiv-congruence-on-name
  (implies (modname-equiv name name-equiv)
           (equal (update-elab-mod$a->name name elab-mod$a)
                  (update-elab-mod$a->name name-equiv elab-mod$a)))
  :rule-classes :congruence)

Theorem: update-elab-mod$a->name-of-elab-mod$a-fix-elab-mod$a

(defthm update-elab-mod$a->name-of-elab-mod$a-fix-elab-mod$a
  (equal (update-elab-mod$a->name name (elab-mod$a-fix elab-mod$a))
         (update-elab-mod$a->name name elab-mod$a)))

Theorem: update-elab-mod$a->name-elab-mod$a-equiv-congruence-on-elab-mod$a

(defthm
  update-elab-mod$a->name-elab-mod$a-equiv-congruence-on-elab-mod$a
  (implies (elab-mod$a-equiv elab-mod$a elab-mod$a-equiv)
           (equal (update-elab-mod$a->name name elab-mod$a)
                  (update-elab-mod$a->name name elab-mod$a-equiv)))
  :rule-classes :congruence)