		Search-engine friendly clone of the ACL2 documentation.

Function-recursion

Constdecl-callees

Functions called by a constant declaration.

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

Definitions and Theorems

Function: constdecl-callees

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

Theorem: identifier-setp-of-constdecl-callees

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

Theorem: constdecl-callees-of-constdecl-fix-decl

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

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

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