all-lambdas

(in-package "ACL2")

(defines all-lambdas
  :parents (std/system/term-queries)
  :short "Lambda expressions in a term."
  (define all-lambdas
    ((term pseudo-termp) (ans pseudo-lambda-listp))
    :returns (final-ans pseudo-lambda-listp :hyp :guard)
    (b* (((when (variablep term)) ans) ((when (fquotep term)) ans)
        (fn (ffn-symb term))
        (ans (if (flambdap fn)
            (all-lambdas (lambda-body fn) (add-to-set-equal fn ans))
            ans)))
      (all-lambdas-lst (fargs term) ans)))
  (define all-lambdas-lst
    ((terms pseudo-term-listp) (ans pseudo-lambda-listp))
    :returns (final-ans pseudo-lambda-listp :hyp :guard)
    (if (endp terms)
      ans
      (all-lambdas-lst (cdr terms) (all-lambdas (car terms) ans))))
  :verify-guards nil
  ///
  (verify-guards all-lambdas))