Check if an expression or type name is unambiguous.
(expr/tyname-unambp expr/tyname) → yes/no
This fixtype does not appear in the abstract syntax trees, but it is the result of dimb-amb-expr/tyname, so we need to define this predicate to state and prove, by induction, that the disambiguator returns unambiguous abstract syntax.
Function:
(defun expr/tyname-unambp (expr/tyname) (declare (xargs :guard (expr/tyname-p expr/tyname))) (let ((__function__ 'expr/tyname-unambp)) (declare (ignorable __function__)) (expr/tyname-case expr/tyname :expr (expr-unambp expr/tyname.unwrap) :tyname (tyname-unambp expr/tyname.unwrap))))
Theorem:
(defthm booleanp-of-expr/tyname-unambp (b* ((yes/no (expr/tyname-unambp expr/tyname))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm expr/tyname-unambp-of-expr/tyname-fix-expr/tyname (equal (expr/tyname-unambp (expr/tyname-fix expr/tyname)) (expr/tyname-unambp expr/tyname)))
Theorem:
(defthm expr/tyname-unambp-expr/tyname-equiv-congruence-on-expr/tyname (implies (expr/tyname-equiv expr/tyname expr/tyname-equiv) (equal (expr/tyname-unambp expr/tyname) (expr/tyname-unambp expr/tyname-equiv))) :rule-classes :congruence)