Get the case-insens field from a matchmode.
(matchmode->case-insens x) → case-insens
This is an ordinary field accessor created by defprod.
Function:
(defun matchmode->case-insens$inline (x) (declare (xargs :guard (matchmode-p x))) (declare (xargs :guard t)) (let ((__function__ 'matchmode->case-insens)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x))) (acl2::bool-fix x)) :exec x)))
Theorem:
(defthm booleanp-of-matchmode->case-insens (b* ((case-insens (matchmode->case-insens$inline x))) (booleanp case-insens)) :rule-classes :type-prescription)
Theorem:
(defthm matchmode->case-insens$inline-of-matchmode-fix-x (equal (matchmode->case-insens$inline (matchmode-fix x)) (matchmode->case-insens$inline x)))
Theorem:
(defthm matchmode->case-insens$inline-matchmode-equiv-congruence-on-x (implies (matchmode-equiv x x-equiv) (equal (matchmode->case-insens$inline x) (matchmode->case-insens$inline x-equiv))) :rule-classes :congruence)