Get the comp field from a atj-type-jprimarr.
(atj-type-jprimarr->comp x) → comp
This is an ordinary field accessor created by fty::defprod.
Function:
(defun atj-type-jprimarr->comp$inline (x) (declare (xargs :guard (atj-typep x))) (declare (xargs :guard (equal (atj-type-kind x) :jprimarr))) (let ((__function__ 'atj-type-jprimarr->comp)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and (equal (atj-type-kind x) :jprimarr) x))) (primitive-type-fix (std::da-nth 0 (cdr x)))) :exec (std::da-nth 0 (cdr x)))))
Theorem:
(defthm primitive-typep-of-atj-type-jprimarr->comp (b* ((comp (atj-type-jprimarr->comp$inline x))) (primitive-typep comp)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-jprimarr->comp$inline-of-atj-type-fix-x (equal (atj-type-jprimarr->comp$inline (atj-type-fix x)) (atj-type-jprimarr->comp$inline x)))
Theorem:
(defthm atj-type-jprimarr->comp$inline-atj-type-equiv-congruence-on-x (implies (atj-type-equiv x x-equiv) (equal (atj-type-jprimarr->comp$inline x) (atj-type-jprimarr->comp$inline x-equiv))) :rule-classes :congruence)
Theorem:
(defthm atj-type-jprimarr->comp-when-wrong-kind (implies (not (equal (atj-type-kind x) :jprimarr)) (equal (atj-type-jprimarr->comp x) (primitive-type-fix nil))))