		Search-engine friendly clone of the ACL2 documentation.

Function-recursion

Console-callees

Functions called by a console call.

Signature
(console-callees cnsl) → callees
Arguments: cnsl — Guard (consolep cnsl).
Returns: callees — Type (identifier-setp callees).

Definitions and Theorems

Function: console-callees

(defun console-callees (cnsl)
  (declare (xargs :guard (consolep cnsl)))
  (let ((__function__ 'console-callees))
    (declare (ignorable __function__))
    (console-case cnsl
                  :assert (expression-callees cnsl.arg)
                  :error (expression-list-callees cnsl.exprs)
                  :log (expression-list-callees cnsl.exprs))))

Theorem: identifier-setp-of-console-callees

(defthm identifier-setp-of-console-callees
  (b* ((callees (console-callees cnsl)))
    (identifier-setp callees))
  :rule-classes :rewrite)

Theorem: console-callees-of-console-fix-cnsl

(defthm console-callees-of-console-fix-cnsl
  (equal (console-callees (console-fix cnsl))
         (console-callees cnsl)))

Theorem: console-callees-console-equiv-congruence-on-cnsl

(defthm console-callees-console-equiv-congruence-on-cnsl
  (implies (console-equiv cnsl cnsl-equiv)
           (equal (console-callees cnsl)
                  (console-callees cnsl-equiv)))
  :rule-classes :congruence)