Issue a badge for a function so `apply$` can evaluate with it

It is best to be somewhat familiar with the documentation of `apply$` before reading this topic.

Before using `defun$` that relies on
it:

(include-book "projects/apply/top" :dir :system)

It is easy to confuse badges, which are issued by `defwarrant`. Badges and
warrants are necessary to ACL2's support of `apply$` because ACL2 is
actually first-order, functions cannot be passed around as objects, ordinary
symbols play the role of ``function objects,'' and somehow the logic must
allow the association of a symbol with the function it names. Furthermore,
to insure the consistency of the logic `introduction-to-apply$`. But to determine whether a newly defined function
is allowed to be known to **Lesson 12** of introduction-to-apply$).

Roughly speaking, badges are about syntax and warrants are about
semantics. The badge for a symbol is a data structure in the ACL2 system
that records information like whether the symbol names a known ACL2 function,
how many arguments that function takes, how many results it returns, which
arguments are treated like function objects to be `apply$`'d, which are
treated like expressions to be `ev$`'d, and which are treated like
ordinary ACL2 objects to be

Both `defun` and `defthm`,
query the world or build and test prototypes, and (b) allow

General Form: (defbadge fn)

where `program`
or `logic` mode. This command analyzes the body of `ev$`, and which are neither. The
conditions checked are sufficient to allow `apply$` to run the function
safely at the top level of the ACL2 read-eval-print loop. However, in order
to prove anything about a call of `logic` mode, as discussed
above — `defwarrant`.

The first condition on `defchoose` or `encapsulate`. In
addition, `sys-call` (which
requires a trust tag) or an untouchable. (For technical reasons,
untouchables are disallowed even if they are on `remove-untouchable`.)

The other conditions depend on whether `apply$` is reachable from

If `mutual-recursion`. The current badging machinery is
unable to enforce the syntactic restrictions for mutually-recursive cliques.
Another restriction is that every function mentioned in the body of `apply$` and other
scions. The basic idea of this last restriction is to make sure that
`lambda`
object. This restriction is enforced by checking the following
conditions:

*(a)* It must be possible for each formal of

*(b)* Every `well-formed-lambda-objectp`.)

This completes the list of restrictions imposed by

Note that if

After a successful `badge` will return the computed badge (when executed in the top-level loop)
and `apply$` will be able to accept the

(include-book "projects/apply/top" :dir :system) (defun foldr (lst fn init) (declare (xargs :mode :program)) (if (endp lst) init (apply$ fn (list (car lst) (foldr (cdr lst) fn init)))))

Note the

ACL2 !>(foldr '(a b c) 'cons '(d e f)) (A B C D E F)

Since

(apply$ 'foldr (list '(a b c) 'cons '(d e f))) ACL2 Error in TOP-LEVEL: The value of APPLY$-USERFN is not specified on FOLDR because FOLDR has not been badged.

However, we can use `badge`. We can successfully apply

ACL2 !>(defbadge foldr) FOLDR now has the badge (APPLY$-BADGE 3 1 NIL :FN NIL) but has no warrant. T ACL2 !>(badge 'foldr) (APPLY$-BADGE 3 1 NIL :FN NIL) ACL2 !>(apply$ 'foldr (list '(a b c) 'cons '(d e f))) (A B C D E F) ACL2 !>(foldr '((a b c) (d e) (f g h) (i j k)) (lambda$ (x y) (foldr x 'cons y)) nil) (A B C D E F G H I J K)

We now clarify the test that we colloquially described above as whether

Since the only system functions that call

The test and the onerous conditions imposed when `apply$`, including ``Limited
Second-Order Functionality in a First-Order Setting'' by Matt Kaufmann
and J Strother Moore and offer a fully fleshed out metalevel proof that
`Essay on Admitting a Model for Apply$ and the Functions that Use
It` in the ACL2 source file

But badges are more concerned with syntax (and, for

ACL2 !>(verify-termination foldr) [Successful. Output deleted.] FOLDR ACL2 !>(thm (equal (apply$ 'foldr (list x 'cons z)) (append x z))) [Unsuccessful. Output deleted.] ******** FAILED ******** ACL2 !>(thm (equal (badge 'foldr) '(APPLY$-BADGE 3 1 NIL :FN NIL))) [Unsuccessful. Output deleted.] ******** FAILED ********

In order to prove anything nontrivial about `warrant` for `defwarrant`. If we execute (defwarrant foldr) and then
amend the failed

If a formal variable (or its slot among the actuals) has an ilk of

The key to the inductive correctness of the algorithm implicity described
below is the fact that when the ACL2 logic is being booted up the only
function symbol with a slot of ilk

Let *v * be the *i *th formal parameter of a defined function
*fn*. Then the ilk of *v * is *v *
eventually makes its way into the first argument of *v * in a slot of ilk *v * is never used
any other way: every place *v * occurs in the body of *fn * is in a
slot of ilk *fn *,
*v * is passed identically in the *i *th argument position of the
call. We say such a *v * is ``used (exclusively) as a function.''

The *i *th formal variable *v * has ilk *v * is ``used (exclusively) as an
expression.'' Note: `ev$` is the natural notion of expression
evaluation in this context: look up the values of variables in the alist
argument to `tamep`.

The *i *th formal variable *v * has ilk *v * is ``used (exclusively) as an ordinary object.''