Ev$
Evaluate a tame expression using apply$
When apply$, actually apply$-lambda, is asked to
apply a LAMBDA object to some arguments it calls ev$ on the body of
the object and an alist binding the formals of the object to the arguments.
Roughly put, ev$ ``works'' by looking up symbols, returning quoted
objects, and using apply$ to apply function symbols to the results of
evaluating their arguments. Ev$ and its clique-mate ev$-list are
mutually-recursive with apply$. Ev$ can only evaluate ``as
expected'' on tame expressions and requires warrants, explicit
in the proof theory or implicit in the evaluation theory, to determine badges and thus tameness. See apply$ for details, including the
formal definitions of ev$ and ev$-list. For a summary of how the
rewriter handles apply$, ev$, and loop$ scions, see
rewriting-calls-of-apply$-ev$-and-loop$-scions.
