		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-unambp

Expr/tyname-unambp

Signature
(expr/tyname-unambp expr/tyname) → fty::result
Arguments: expr/tyname — Guard (expr/tyname-p expr/tyname).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: expr/tyname-unambp

(defun expr/tyname-unambp (expr/tyname)
  (declare (xargs :guard (expr/tyname-p expr/tyname)))
  (declare (ignorable expr/tyname))
  (let ((__function__ 'expr/tyname-unambp))
    (declare (ignorable __function__))
    (expr/tyname-case
         expr/tyname
         :expr (expr-unambp (expr/tyname-expr->expr expr/tyname))
         :tyname
         (tyname-unambp (expr/tyname-tyname->tyname expr/tyname)))))

Theorem: booleanp-of-expr/tyname-unambp

(defthm booleanp-of-expr/tyname-unambp
  (b* ((fty::result (expr/tyname-unambp expr/tyname)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: expr/tyname-unambp-of-expr/tyname-fix-expr/tyname

(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: expr/tyname-unambp-expr/tyname-equiv-congruence-on-expr/tyname

(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)