Check if a list of declarations is unambiguous.
(decl-list-unambp x) → std::bool
This is an ordinary std::deflist. It is
"loose" in that it does not care whether
Function:
(defun decl-list-unambp (x) (declare (xargs :guard (decl-listp x))) (let ((__function__ 'decl-list-unambp)) (declare (ignorable __function__)) (if (consp x) (and (decl-unambp (car x)) (decl-list-unambp (cdr x))) t)))
Theorem:
(defthm decl-list-unambp-of-decl-list-fix-x (equal (decl-list-unambp (decl-list-fix x)) (decl-list-unambp x)))
Theorem:
(defthm decl-list-unambp-decl-list-equiv-congruence-on-x (implies (decl-list-equiv x x-equiv) (equal (decl-list-unambp x) (decl-list-unambp x-equiv))) :rule-classes :congruence)