		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-modinst$c-fix

Signature
(elab-modinst$c-fix elab-modinst$c) → elab-modinst$c

Definitions and Theorems

Function: elab-modinst$c-fix$inline

(defun elab-modinst$c-fix$inline (elab-modinst$c)
  (declare (xargs :stobjs (elab-modinst$c)))
  (declare (xargs :guard t))
  (let ((__function__ 'elab-modinst$c-fix))
    (declare (ignorable __function__))
    (mbe :logic (non-exec (elab-modinst-fix elab-modinst$c))
         :exec elab-modinst$c)))

Theorem: elab-modinst$c-fix$inline-of-elab-modinst-fix-elab-modinst$c

(defthm elab-modinst$c-fix$inline-of-elab-modinst-fix-elab-modinst$c
  (equal
       (elab-modinst$c-fix$inline (elab-modinst-fix elab-modinst$c))
       (elab-modinst$c-fix$inline elab-modinst$c)))

Theorem: elab-modinst$c-fix$inline-elab-modinst$c-equiv-congruence-on-elab-modinst$c

(defthm
 elab-modinst$c-fix$inline-elab-modinst$c-equiv-congruence-on-elab-modinst$c
 (implies (elab-modinst$c-equiv elab-modinst$c elab-modinst$c-equiv)
          (equal (elab-modinst$c-fix$inline elab-modinst$c)
                 (elab-modinst$c-fix$inline elab-modinst$c-equiv)))
 :rule-classes :congruence)