		Search-engine friendly clone of the ACL2 documentation.

Dirabsdeclor-array-static1

Dirabsdeclor-array-static1->size

Get the size field from a dirabsdeclor-array-static1.

Signature
(dirabsdeclor-array-static1->size x) → size
Arguments: x — Guard (dirabsdeclorp x).
Returns: size — Type (exprp size).

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

Definitions and Theorems

Function: dirabsdeclor-array-static1->size$inline

(defun dirabsdeclor-array-static1->size$inline (x)
  (declare (xargs :guard (dirabsdeclorp x)))
  (declare (xargs :guard (equal (dirabsdeclor-kind x)
                                :array-static1)))
  (mbe :logic
       (b* ((x (and (equal (dirabsdeclor-kind x)
                           :array-static1)
                    x)))
         (expr-fix (cdr (cdr (cdr x)))))
       :exec (cdr (cdr (cdr x)))))

Theorem: exprp-of-dirabsdeclor-array-static1->size

(defthm exprp-of-dirabsdeclor-array-static1->size
  (b* ((size (dirabsdeclor-array-static1->size$inline x)))
    (exprp size))
  :rule-classes :rewrite)

Theorem: dirabsdeclor-array-static1->size$inline-of-dirabsdeclor-fix-x

(defthm
      dirabsdeclor-array-static1->size$inline-of-dirabsdeclor-fix-x
 (equal
      (dirabsdeclor-array-static1->size$inline (dirabsdeclor-fix x))
      (dirabsdeclor-array-static1->size$inline x)))

Theorem: dirabsdeclor-array-static1->size$inline-dirabsdeclor-equiv-congruence-on-x

(defthm
 dirabsdeclor-array-static1->size$inline-dirabsdeclor-equiv-congruence-on-x
 (implies (dirabsdeclor-equiv x x-equiv)
          (equal (dirabsdeclor-array-static1->size$inline x)
                 (dirabsdeclor-array-static1->size$inline x-equiv)))
 :rule-classes :congruence)

Theorem: dirabsdeclor-array-static1->size-when-wrong-kind

(defthm dirabsdeclor-array-static1->size-when-wrong-kind
  (implies (not (equal (dirabsdeclor-kind x)
                       :array-static1))
           (equal (dirabsdeclor-array-static1->size x)
                  (expr-fix nil))))