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