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