		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$a-wirename->idx

Signature
(elab-mod$a-wirename->idx name elab-mod$a) → *
Arguments: name — Guard (name-p name).; elab-mod$a — Guard (elab-mod$ap elab-mod$a).

Definitions and Theorems

Function: elab-mod$a-wirename->idx

(defun elab-mod$a-wirename->idx (name elab-mod$a)
  (declare (xargs :guard (and (name-p name)
                              (elab-mod$ap elab-mod$a))))
  (let ((__function__ 'elab-mod$a-wirename->idx))
    (declare (ignorable __function__))
    (index-of
         (name-fix name)
         (wirelist->names (g :wires (elab-mod$a-fix elab-mod$a))))))

Theorem: elab-mod$a-wirename->idx-of-name-fix-name

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

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

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

Theorem: elab-mod$a-wirename->idx-of-elab-mod$a-fix-elab-mod$a

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

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

(defthm
 elab-mod$a-wirename->idx-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-wirename->idx name elab-mod$a)
                 (elab-mod$a-wirename->idx name elab-mod$a-equiv)))
 :rule-classes :congruence)