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