		Search-engine friendly clone of the ACL2 documentation.

Function-recursion

Vardecl-callees

Functions called by a variable declaration.

Signature
(vardecl-callees decl) → callees
Arguments: decl — Guard (vardeclp decl).
Returns: callees — Type (identifier-setp callees).

Definitions and Theorems

Function: vardecl-callees

(defun vardecl-callees (decl)
  (declare (xargs :guard (vardeclp decl)))
  (let ((__function__ 'vardecl-callees))
    (declare (ignorable __function__))
    (expression-callees (vardecl->init decl))))

Theorem: identifier-setp-of-vardecl-callees

(defthm identifier-setp-of-vardecl-callees
  (b* ((callees (vardecl-callees decl)))
    (identifier-setp callees))
  :rule-classes :rewrite)

Theorem: vardecl-callees-of-vardecl-fix-decl

(defthm vardecl-callees-of-vardecl-fix-decl
  (equal (vardecl-callees (vardecl-fix decl))
         (vardecl-callees decl)))

Theorem: vardecl-callees-vardecl-equiv-congruence-on-decl

(defthm vardecl-callees-vardecl-equiv-congruence-on-decl
  (implies (vardecl-equiv decl decl-equiv)
           (equal (vardecl-callees decl)
                  (vardecl-callees decl-equiv)))
  :rule-classes :congruence)