		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Update-moddb->nmods

Signature
(update-moddb->nmods n moddb) → moddb
Arguments: n — Guard (natp n).

Definitions and Theorems

Function: update-moddb->nmods$inline

(defun update-moddb->nmods$inline (n moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'update-moddb->nmods))
    (declare (ignorable __function__))
    (mbe :logic (non-exec (update-nth *moddb->nmods* (nfix n)
                                      (moddb-fix moddb)))
         :exec (update-moddb->nmods1 n moddb))))

Theorem: update-moddb->nmods$inline-of-nfix-n

(defthm update-moddb->nmods$inline-of-nfix-n
  (equal (update-moddb->nmods$inline (nfix n)
                                     moddb)
         (update-moddb->nmods$inline n moddb)))

Theorem: update-moddb->nmods$inline-nat-equiv-congruence-on-n

(defthm update-moddb->nmods$inline-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (update-moddb->nmods$inline n moddb)
                  (update-moddb->nmods$inline n-equiv moddb)))
  :rule-classes :congruence)

Theorem: update-moddb->nmods$inline-of-moddb-fix-moddb

(defthm update-moddb->nmods$inline-of-moddb-fix-moddb
  (equal (update-moddb->nmods$inline n (moddb-fix moddb))
         (update-moddb->nmods$inline n moddb)))

Theorem: update-moddb->nmods$inline-moddb-equiv-congruence-on-moddb

(defthm update-moddb->nmods$inline-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (update-moddb->nmods$inline n moddb)
                  (update-moddb->nmods$inline n moddb-equiv)))
  :rule-classes :congruence)