Check if a declarator or abstract declarator is unambiguous.
(declor/absdeclor-unambp declor/absdeclor) → yes/no
The purpose of this predicate is similar to expr/tyname-unambp: see its documentation.
Function:
(defun declor/absdeclor-unambp (declor/absdeclor) (declare (xargs :guard (declor/absdeclor-p declor/absdeclor))) (let ((__function__ 'declor/absdeclor-unambp)) (declare (ignorable __function__)) (declor/absdeclor-case declor/absdeclor :declor (declor-unambp declor/absdeclor.unwrap) :absdeclor (absdeclor-unambp declor/absdeclor.unwrap))))
Theorem:
(defthm booleanp-of-declor/absdeclor-unambp (b* ((yes/no (declor/absdeclor-unambp declor/absdeclor))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm declor/absdeclor-unambp-of-declor/absdeclor-fix-declor/absdeclor (equal (declor/absdeclor-unambp (declor/absdeclor-fix declor/absdeclor)) (declor/absdeclor-unambp declor/absdeclor)))
Theorem:
(defthm declor/absdeclor-unambp-declor/absdeclor-equiv-congruence-on-declor/absdeclor (implies (declor/absdeclor-equiv declor/absdeclor declor/absdeclor-equiv) (equal (declor/absdeclor-unambp declor/absdeclor) (declor/absdeclor-unambp declor/absdeclor-equiv))) :rule-classes :congruence)