		Search-engine friendly clone of the ACL2 documentation.

Pseudo-lambda

Pseudo-lambda->formals

Signature
(pseudo-lambda->formals x) → formals
Arguments: x — Guard (pseudo-lambda-p x).
Returns: formals — Type (symbol-listp formals).

Definitions and Theorems

Function: pseudo-lambda->formals

(defun pseudo-lambda->formals (x)
  (declare (xargs :guard (pseudo-lambda-p x)))
  (let ((__function__ 'pseudo-lambda->formals))
    (declare (ignorable __function__))
    (mbe :logic (replace-non-symbols-with-nil (cadr x))
         :exec (cadr x))))

Theorem: symbol-listp-of-pseudo-lambda->formals

(defthm symbol-listp-of-pseudo-lambda->formals
  (b* ((formals (pseudo-lambda->formals x)))
    (symbol-listp formals))
  :rule-classes :rewrite)

Theorem: pseudo-lambda->formals-of-pseudo-lambda-fix-x

(defthm pseudo-lambda->formals-of-pseudo-lambda-fix-x
  (equal (pseudo-lambda->formals (pseudo-lambda-fix x))
         (pseudo-lambda->formals x)))

Theorem: pseudo-lambda->formals-pseudo-lambda-equiv-congruence-on-x

(defthm pseudo-lambda->formals-pseudo-lambda-equiv-congruence-on-x
  (implies (pseudo-lambda-equiv x x-equiv)
           (equal (pseudo-lambda->formals x)
                  (pseudo-lambda->formals x-equiv)))
  :rule-classes :congruence)