		Search-engine friendly clone of the ACL2 documentation.

Pseudo-term-lambda

Pseudo-term-lambda->fn

Accessor for the function of a lambda call pseudo-term.

Signature
(pseudo-term-lambda->fn x) → fn
Arguments: x — Guard (pseudo-termp x).
Returns: fn — Type (pseudo-lambda-p fn).

Definitions and Theorems

Function: pseudo-term-lambda->fn

(defun pseudo-term-lambda->fn (x)
 (declare (xargs :guard (pseudo-termp x)))
 (declare (xargs :guard (eq (pseudo-term-kind x) :lambda)))
 (let ((__function__ 'pseudo-term-lambda->fn))
  (declare (ignorable __function__))
  (mbe
    :logic (pseudo-lambda-fix (and (eq (pseudo-term-kind x) :lambda)
                                   (car x)))
    :exec (car x))))

Theorem: pseudo-lambda-p-of-pseudo-term-lambda->fn

(defthm pseudo-lambda-p-of-pseudo-term-lambda->fn
  (b* ((fn (pseudo-term-lambda->fn x)))
    (pseudo-lambda-p fn))
  :rule-classes :rewrite)

Theorem: pseudo-term-lambda->fn-of-pseudo-term-fix-x

(defthm pseudo-term-lambda->fn-of-pseudo-term-fix-x
  (equal (pseudo-term-lambda->fn (pseudo-term-fix x))
         (pseudo-term-lambda->fn x)))

Theorem: pseudo-term-lambda->fn-pseudo-term-equiv-congruence-on-x

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