		Search-engine friendly clone of the ACL2 documentation.

Inst

Inst->fn

Get the fn field from a inst.

Signature
(inst->fn x) → fn
Arguments: x — Guard (inst-p x).
Returns: fn — Type (fn-desc-p fn).

This is an ordinary field accessor created by defprod.

Definitions and Theorems

Function: inst->fn$inline

(defun inst->fn$inline (x)
 (declare (xargs :guard (inst-p x)))
 (declare (xargs :guard t))
 (let ((__function__ 'inst->fn))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b* ((x (and t x)))
    (fn-desc-fix (std::prod-car (std::prod-cdr (std::prod-cdr x)))))
   :exec (std::prod-car (std::prod-cdr (std::prod-cdr x))))))

Theorem: fn-desc-p-of-inst->fn

(defthm fn-desc-p-of-inst->fn
  (b* ((fn (inst->fn$inline x)))
    (fn-desc-p fn))
  :rule-classes :rewrite)

Theorem: inst->fn$inline-of-inst-fix-x

(defthm inst->fn$inline-of-inst-fix-x
  (equal (inst->fn$inline (inst-fix x))
         (inst->fn$inline x)))

Theorem: inst->fn$inline-inst-equiv-congruence-on-x

(defthm inst->fn$inline-inst-equiv-congruence-on-x
  (implies (inst-equiv x x-equiv)
           (equal (inst->fn$inline x)
                  (inst->fn$inline x-equiv)))
  :rule-classes :congruence)