Recognize well-formed event forms.
Here we formalize some constraints on untranslated event forms.
Because of macros it is almost impossible
to put constraints on event forms.
For example, with an appropriate defmacro of
The most rigorous test would translate the alleged form, but that would require state and the specification of translate's many options like whether stobjs are treated specially. Until we need it, we are not going to try to formalize the stronger test.
(defun pseudo-event-formp (x) (declare (xargs :guard t)) (and (consp x) (true-listp x) (symbolp (car x))))