		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-unambp

Declon/stmt-unambp

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

Definitions and Theorems

Function: declon/stmt-unambp

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

Theorem: booleanp-of-declon/stmt-unambp

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

Theorem: declon/stmt-unambp-of-declon/stmt-fix-declon/stmt

(defthm declon/stmt-unambp-of-declon/stmt-fix-declon/stmt
  (equal (declon/stmt-unambp (declon/stmt-fix declon/stmt))
         (declon/stmt-unambp declon/stmt)))

Theorem: declon/stmt-unambp-declon/stmt-equiv-congruence-on-declon/stmt

(defthm
     declon/stmt-unambp-declon/stmt-equiv-congruence-on-declon/stmt
  (implies (declon/stmt-equiv declon/stmt declon/stmt-equiv)
           (equal (declon/stmt-unambp declon/stmt)
                  (declon/stmt-unambp declon/stmt-equiv)))
  :rule-classes :congruence)