		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod-fix

Signature
(elab-mod-fix elab-mod) → elab-mod

Definitions and Theorems

Function: elab-mod-fix$inline

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

Theorem: elab-mod-fix$inline-of-elab-mod$a-fix-elab-mod

(defthm elab-mod-fix$inline-of-elab-mod$a-fix-elab-mod
  (equal (elab-mod-fix$inline (elab-mod$a-fix elab-mod))
         (elab-mod-fix$inline elab-mod)))

Theorem: elab-mod-fix$inline-elab-mod$a-equiv-congruence-on-elab-mod

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