		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-path->wiredecl

Signature
(moddb-path->wiredecl path modidx moddb) → wire
Arguments: path — Guard (path-p path).; modidx — Guard (natp modidx).; moddb — Guard (moddb-ok moddb).
Returns: wire — Type (iff (wire-p wire) wire).

Definitions and Theorems

Function: moddb-path->wiredecl

(defun moddb-path->wiredecl (path modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (path-p path)
                              (natp modidx)
                              (moddb-ok moddb))))
  (declare (xargs :guard (< modidx (moddb->nmods moddb))))
  (let ((__function__ 'moddb-path->wiredecl))
    (declare (ignorable __function__))
    (b* (((mv err wire & bitsel)
          (moddb-path->wireidx/decl path modidx moddb))
         ((when err) (raise "~@0" err))
         ((when bitsel)
          (raise "Didn't expect a bit select: ~x0"
                 path)))
      wire)))

Theorem: return-type-of-moddb-path->wiredecl

(defthm return-type-of-moddb-path->wiredecl
  (b* ((wire (moddb-path->wiredecl path modidx moddb)))
    (iff (wire-p wire) wire))
  :rule-classes :rewrite)

Theorem: moddb-path->wiredecl-iff-wireidx

(defthm moddb-path->wiredecl-iff-wireidx
  (iff (moddb-path->wiredecl path modidx moddb)
       (moddb-path->wireidx path modidx moddb)))

Theorem: moddb-path->wiredecl-of-path-fix-path

(defthm moddb-path->wiredecl-of-path-fix-path
  (equal (moddb-path->wiredecl (path-fix path)
                               modidx moddb)
         (moddb-path->wiredecl path modidx moddb)))

Theorem: moddb-path->wiredecl-path-equiv-congruence-on-path

(defthm moddb-path->wiredecl-path-equiv-congruence-on-path
  (implies (path-equiv path path-equiv)
           (equal (moddb-path->wiredecl path modidx moddb)
                  (moddb-path->wiredecl path-equiv modidx moddb)))
  :rule-classes :congruence)

Theorem: moddb-path->wiredecl-of-nfix-modidx

(defthm moddb-path->wiredecl-of-nfix-modidx
  (equal (moddb-path->wiredecl path (nfix modidx)
                               moddb)
         (moddb-path->wiredecl path modidx moddb)))

Theorem: moddb-path->wiredecl-nat-equiv-congruence-on-modidx

(defthm moddb-path->wiredecl-nat-equiv-congruence-on-modidx
  (implies (nat-equiv modidx modidx-equiv)
           (equal (moddb-path->wiredecl path modidx moddb)
                  (moddb-path->wiredecl path modidx-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-path->wiredecl-of-moddb-fix-moddb

(defthm moddb-path->wiredecl-of-moddb-fix-moddb
  (equal (moddb-path->wiredecl path modidx (moddb-fix moddb))
         (moddb-path->wiredecl path modidx moddb)))

Theorem: moddb-path->wiredecl-moddb-equiv-congruence-on-moddb

(defthm moddb-path->wiredecl-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-path->wiredecl path modidx moddb)
                  (moddb-path->wiredecl path modidx moddb-equiv)))
  :rule-classes :congruence)