		Search-engine friendly clone of the ACL2 documentation.

Addresses

Ast-addresses-valid?

Signature
(ast-addresses-valid? ast) → y/n
Returns: y/n — Type (booleanp y/n).

Definitions and Theorems

Function: ast-addresses-valid?

(defun ast-addresses-valid? (ast)
  (declare (xargs :guard t))
  (let ((__function__ 'ast-addresses-valid?))
    (declare (ignorable __function__))
    (all-addresses-valid? (find-addresses ast))))

Theorem: booleanp-of-ast-addresses-valid?

(defthm booleanp-of-ast-addresses-valid?
  (b* ((y/n (ast-addresses-valid? ast)))
    (booleanp y/n))
  :rule-classes :rewrite)