		Search-engine friendly clone of the ACL2 documentation.

Dirabsdeclor-array-static2

Dirabsdeclor-array-static2->declor?

Get the declor? field from a dirabsdeclor-array-static2.

Signature
(dirabsdeclor-array-static2->declor? x) → declor?
Arguments: x — Guard (dirabsdeclorp x).
Returns: declor? — Type (dirabsdeclor-optionp declor?).

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

Definitions and Theorems

Function: dirabsdeclor-array-static2->declor?$inline

(defun dirabsdeclor-array-static2->declor?$inline (x)
  (declare (xargs :guard (dirabsdeclorp x)))
  (declare (xargs :guard (equal (dirabsdeclor-kind x)
                                :array-static2)))
  (mbe :logic
       (b* ((x (and (equal (dirabsdeclor-kind x)
                           :array-static2)
                    x)))
         (dirabsdeclor-option-fix (car (cdr x))))
       :exec (car (cdr x))))

Theorem: dirabsdeclor-optionp-of-dirabsdeclor-array-static2->declor?

(defthm dirabsdeclor-optionp-of-dirabsdeclor-array-static2->declor?
  (b* ((declor? (dirabsdeclor-array-static2->declor?$inline x)))
    (dirabsdeclor-optionp declor?))
  :rule-classes :rewrite)

Theorem: dirabsdeclor-array-static2->declor?$inline-of-dirabsdeclor-fix-x

(defthm
   dirabsdeclor-array-static2->declor?$inline-of-dirabsdeclor-fix-x
 (equal
   (dirabsdeclor-array-static2->declor?$inline (dirabsdeclor-fix x))
   (dirabsdeclor-array-static2->declor?$inline x)))

Theorem: dirabsdeclor-array-static2->declor?$inline-dirabsdeclor-equiv-congruence-on-x

(defthm
 dirabsdeclor-array-static2->declor?$inline-dirabsdeclor-equiv-congruence-on-x
 (implies
      (dirabsdeclor-equiv x x-equiv)
      (equal (dirabsdeclor-array-static2->declor?$inline x)
             (dirabsdeclor-array-static2->declor?$inline x-equiv)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-array-static2->declor?-when-wrong-kind

(defthm dirabsdeclor-array-static2->declor?-when-wrong-kind
  (implies (not (equal (dirabsdeclor-kind x)
                       :array-static2))
           (equal (dirabsdeclor-array-static2->declor? x)
                  (dirabsdeclor-option-fix nil))))