		Search-engine friendly clone of the ACL2 documentation.

Pinst-flat

Pinst-flat->guts

Get the guts field from a pinst-flat.

Signature
(pinst-flat->guts x) → guts
Arguments: x — Guard (pinst-p x).
Returns: guts — Type (pflat-p guts).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: pinst-flat->guts$inline

(defun pinst-flat->guts$inline (x)
  (declare (xargs :guard (pinst-p x)))
  (declare (xargs :guard (equal (pinst-kind x) :flat)))
  (let ((acl2::__function__ 'pinst-flat->guts))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and (equal (pinst-kind x) :flat) x)))
           (pflat-fix (cdr x)))
         :exec (cdr x))))

Theorem: pflat-p-of-pinst-flat->guts

(defthm pflat-p-of-pinst-flat->guts
  (b* ((guts (pinst-flat->guts$inline x)))
    (pflat-p guts))
  :rule-classes :rewrite)

Theorem: pinst-flat->guts$inline-of-pinst-fix-x

(defthm pinst-flat->guts$inline-of-pinst-fix-x
  (equal (pinst-flat->guts$inline (pinst-fix x))
         (pinst-flat->guts$inline x)))

Theorem: pinst-flat->guts$inline-pinst-equiv-congruence-on-x

(defthm pinst-flat->guts$inline-pinst-equiv-congruence-on-x
  (implies (pinst-equiv x x-equiv)
           (equal (pinst-flat->guts$inline x)
                  (pinst-flat->guts$inline x-equiv)))
  :rule-classes :congruence)

Theorem: pinst-flat->guts-when-wrong-kind

(defthm pinst-flat->guts-when-wrong-kind
  (implies (not (equal (pinst-kind x) :flat))
           (equal (pinst-flat->guts x)
                  (pflat-fix nil))))