		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-modidx-get-name

Signature
(moddb-modidx-get-name idx moddb) → *
Arguments: idx — Guard (natp idx).

Definitions and Theorems

Function: moddb-modidx-get-name

(defun moddb-modidx-get-name (idx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (natp idx)))
  (declare (xargs :guard (and (moddb-basics-ok moddb)
                              (< idx (moddb->nmods moddb)))))
  (let ((__function__ 'moddb-modidx-get-name))
    (declare (ignorable __function__))
    (b* (((stobj-get name)
          ((elab-mod (moddb->modsi idx moddb)))
          (elab-mod->name elab-mod)))
      name)))

Theorem: moddb-modidx-get-name-of-nfix-idx

(defthm moddb-modidx-get-name-of-nfix-idx
  (equal (moddb-modidx-get-name (nfix idx) moddb)
         (moddb-modidx-get-name idx moddb)))

Theorem: moddb-modidx-get-name-nat-equiv-congruence-on-idx

(defthm moddb-modidx-get-name-nat-equiv-congruence-on-idx
  (implies (nat-equiv idx idx-equiv)
           (equal (moddb-modidx-get-name idx moddb)
                  (moddb-modidx-get-name idx-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-modidx-get-name-of-moddb-fix-moddb

(defthm moddb-modidx-get-name-of-moddb-fix-moddb
  (equal (moddb-modidx-get-name idx (moddb-fix moddb))
         (moddb-modidx-get-name idx moddb)))

Theorem: moddb-modidx-get-name-moddb-equiv-congruence-on-moddb

(defthm moddb-modidx-get-name-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-modidx-get-name idx moddb)
                  (moddb-modidx-get-name idx moddb-equiv)))
  :rule-classes :congruence)