Introduce an evaluator function

Example: (defevaluator evl evl-list ((length x) (member-equal x y)))

See meta.

General Form: (defevaluator ev ev-list ((g1 x1 ... xn_1) ... (gk x1 ... xn_k)) :namedp flg) ; [optional keyword argument]

where

This function provides a convenient way to constrain

If the *ev**i*, e.g.,

`encapsulate` after generating the
appropriate `defun` and `defthm` events. Perhaps the easiest way
to understand what

:trans1 (defevaluator evl evl-list ((length x) (member-equal x y)))

and inspect the output. This trick is also useful in the rare case that
the event fails because a hint is needed. In that case, the output of
`trans1` can be edited by adding hints, then submitted
directly.

Formally,

*i* in the generated
constraint names are the parenthesized numbers below. When

(0) How to ev an arbitrary function application: [EV-OF-FNCALL-ARGS] (implies (and (consp x) (syntaxp (not (equal a ''nil))) (not (equal (car x) 'quote))) (equal (ev x a) (ev (cons (car x) (kwote-lst (ev-list (cdr x) a))) nil))) (1) How to ev a variable symbol: [EV-OF-VARIABLE] (implies (symbolp x) (equal (ev x a) (and x (cdr (assoc-equal x a))))) (2) How to ev a constant: [EV-OF-QUOTE] (implies (and (consp x) (equal (car x) 'quote)) (equal (ev x a) (cadr x))) (3) How to ev a lambda application: [EV-OF-LAMBDA] (implies (and (consp x) (consp (car x))) (equal (ev x a) (ev (caddar x) (pairlis$ (cadar x) (ev-list (cdr x) a))))) (4) How to ev an empty argument list: [EV-LIST-OF-ATOM] (implies (not (consp x-lst)) (equal (ev-list x-lst a) nil)) (5) How to ev a non-empty argument list: [EV-LIST-OF-CONS] (implies (consp x-lst) (equal (ev-list x-lst a) (cons (ev (car x-lst) a) (ev-list (cdr x-lst) a)))) (6) How to ev a non-symbol atom: [EV-OF-NONSYMBOL-ATOM] (implies (and (not (consp x)) (not (symbolp x))) (equal (ev x a) nil)) (7) How to ev a cons whose car is a non-symbol atom: [EV-OF-BAD-FNCALL] (implies (and (consp x) (not (consp (car x))) (not (symbolp (car x)))) (equal (ev x a) nil)) (k) For each i from 1 to k, how to ev an application of gi, where gi is a function symbol of n arguments: [EV-OF-gi-CALL] (implies (and (consp x) (equal (car x) 'gi)) (equal (ev x a) (gi (ev x1 a) ... (ev xn a)))), where xi is the (cad...dr x) expression equivalent to (nth i x).

(Aside: (3) above may seem surprising, since the bindings of *closed*: in

Acknowledgment: We thank Sol Swords and Jared Davis for their community
book

- Defevaluator-fast
- Formerly a faster alternative to defevaluator, now just an alias.