Check if a function definition is unambiguous.
Function:
(defun fundef-unambp (fundef) (declare (xargs :guard (fundefp fundef))) (let ((__function__ 'fundef-unambp)) (declare (ignorable __function__)) (and (declspec-list-unambp (fundef->spec fundef)) (declor-unambp (fundef->declor fundef)) (decl-list-unambp (fundef->decls fundef)) (stmt-unambp (fundef->body fundef)))))
Theorem:
(defthm booleanp-of-fundef-unambp (b* ((yes/no (fundef-unambp fundef))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm declspec-list-unambp-of-fundef->spec (implies (fundef-unambp fundef) (declspec-list-unambp (fundef->spec fundef))))
Theorem:
(defthm declor-unambp-of-fundef->declor (implies (fundef-unambp fundef) (declor-unambp (fundef->declor fundef))))
Theorem:
(defthm decl-list-unambp-of-fundef->decls (implies (fundef-unambp fundef) (decl-list-unambp (fundef->decls fundef))))
Theorem:
(defthm stmt-unambp-of-fundef->body (implies (fundef-unambp fundef) (stmt-unambp (fundef->body fundef))))
Theorem:
(defthm fundef-unambp-of-fundef-fix-fundef (equal (fundef-unambp (fundef-fix fundef)) (fundef-unambp fundef)))
Theorem:
(defthm fundef-unambp-fundef-equiv-congruence-on-fundef (implies (fundef-equiv fundef fundef-equiv) (equal (fundef-unambp fundef) (fundef-unambp fundef-equiv))) :rule-classes :congruence)