		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$a->instname

Signature
(elab-mod$a->instname idx elab-mod$a) → name
Arguments: idx — Guard (natp idx).; elab-mod$a — Guard (elab-mod$ap elab-mod$a).
Returns: name — Type (name-p name).

Definitions and Theorems

Function: elab-mod$a->instname

(defun elab-mod$a->instname (idx elab-mod$a)
  (declare (xargs :guard (and (natp idx)
                              (elab-mod$ap elab-mod$a))))
  (declare (xargs :guard (< idx (elab-mod$a-ninsts elab-mod$a))))
  (let ((__function__ 'elab-mod$a->instname))
    (declare (ignorable __function__))
    (name-fix (nth *elab-modinst$c->instname*
                   (nth idx
                        (g :insts (elab-mod$a-fix elab-mod$a)))))))

Theorem: name-p-of-elab-mod$a->instname

(defthm name-p-of-elab-mod$a->instname
  (b* ((name (elab-mod$a->instname idx elab-mod$a)))
    (name-p name))
  :rule-classes :rewrite)

Theorem: elab-mod$a->instname-of-nfix-idx

(defthm elab-mod$a->instname-of-nfix-idx
  (equal (elab-mod$a->instname (nfix idx)
                               elab-mod$a)
         (elab-mod$a->instname idx elab-mod$a)))

Theorem: elab-mod$a->instname-nat-equiv-congruence-on-idx

(defthm elab-mod$a->instname-nat-equiv-congruence-on-idx
  (implies (nat-equiv idx idx-equiv)
           (equal (elab-mod$a->instname idx elab-mod$a)
                  (elab-mod$a->instname idx-equiv elab-mod$a)))
  :rule-classes :congruence)

Theorem: elab-mod$a->instname-of-elab-mod$a-fix-elab-mod$a

(defthm elab-mod$a->instname-of-elab-mod$a-fix-elab-mod$a
  (equal (elab-mod$a->instname idx (elab-mod$a-fix elab-mod$a))
         (elab-mod$a->instname idx elab-mod$a)))

Theorem: elab-mod$a->instname-elab-mod$a-equiv-congruence-on-elab-mod$a

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