Lambda object constructor for use with

Intuitively, a quoted

'(LAMBDA (X) (BINARY-+ '1 X))

e.g., a quoted constant beginning with the symbol `Apply$` can handle quoted

One should strive to always enter ``well-formed `well-formed-lambda-objectp` but our hope is that mastering those details is
unnecessary because ACL2 provides a built-in ``macro,''

*terms may only appear in argument slots of ilk*

Examples: (lambda$ (x y) (append x (list y))) (lambda$ (n lst str) (declare (type integer n) (type string str) (xargs :guard (and (posp n) (true-listp lst) (< (- n 1) (length lst))))) (nth (- n 1) lst)) General Form: (lambda$ vars dcl* body)

where the `defun` event with the same formals, declarations
and body. In particular,

The allowed `xargs` keywords allowed are

The translated form of a `lambda` object. For example,

(COLLECT$ '(LAMBDA (X) (DECLARE (IGNORABLE X)) (RETURN-LAST 'PROGN '(LAMBDA$ (X) (+ 1 X)) (BINARY-+ '1 X))) LST)

The

The prover tries to print each quoted `fn-equal`) to
the original `do-loop$`s are involved.

Furthermore, since you are allowed to type in quoted `warrant` has been issued there is probably no
provably equivalent

The main lessons here are

- you should use
lambda$ rather than quotedlambda objects in your prover input, - you should make sure to warrant every user-defined function in your
lambda$ expressions, and - if you see a quoted
lambda object rather than alambda$ expression in your prover output, that quotedlambda object probably involves unwarranted symbols which will make it impossible to prove anything interesting about it.

If you do not want the prover output to give special treatment to quoted

(defattach-system (untranslate-lambda-object-p constant-nil-function-arity-0))

With this attachment, the prover will print all quoted

Quoted *guard verification*), and if the guard holds
of the actuals to which the object is applied (which we call *guard
checking*), a compiled version of the object is run. Otherwise, depending
on how `set-guard-checking` has been configured, either an error is
signalled or the object is interpreted under the axioms defining `print-cl-cache`.

When a guarded quoted

But unlike defined function symbols, whose guards may be verified at

ACL2 !>(apply$ (lambda$ (x) (declare (type (satisfies natp) x)) (* x x)) '(5))

giving

So

To try to verify the guards of a quoted

Interpreting small quoted

But the tau system is pretty weak and so will be unable to verify some
non-trivial guard conjectures, which will mean the `verify-guards`, which as of Version 8.1 takes

(verify-guards (lambda$ (x) (declare (type (satisfies natp) x)) (* x x)))

While this functionality is available to you, deciding that you need to
use it is problematic. `print-cl-cache` provides basic information about
the cache and its documentation may help you discover which