Check if a direct abstract declarator has
a
(dirabsdeclor-decl?-nil-p dirabsdeclor) → yes/no
This excludes the base case(s) of direct abstract declarators.
All the other recursive cases have a
Function:
(defun dirabsdeclor-decl?-nil-p (dirabsdeclor) (declare (xargs :guard (dirabsdeclorp dirabsdeclor))) (let ((__function__ 'dirabsdeclor-decl?-nil-p)) (declare (ignorable __function__)) (dirabsdeclor-case dirabsdeclor :dummy-base nil :paren nil :array (not dirabsdeclor.decl?) :array-static1 (not dirabsdeclor.decl?) :array-static2 (not dirabsdeclor.decl?) :array-star (not dirabsdeclor.decl?) :function (not dirabsdeclor.decl?))))
Theorem:
(defthm booleanp-of-dirabsdeclor-decl?-nil-p (b* ((yes/no (dirabsdeclor-decl?-nil-p dirabsdeclor))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm dirabsdeclor-decl?-nil-p-of-dirabsdeclor-fix-dirabsdeclor (equal (dirabsdeclor-decl?-nil-p (dirabsdeclor-fix dirabsdeclor)) (dirabsdeclor-decl?-nil-p dirabsdeclor)))
Theorem:
(defthm dirabsdeclor-decl?-nil-p-dirabsdeclor-equiv-congruence-on-dirabsdeclor (implies (dirabsdeclor-equiv dirabsdeclor dirabsdeclor-equiv) (equal (dirabsdeclor-decl?-nil-p dirabsdeclor) (dirabsdeclor-decl?-nil-p dirabsdeclor-equiv))) :rule-classes :congruence)