Recognize processed hints inputs of event macros.

- Signature
(evmac-input-hints-p x) → yes/no

- Returns
`yes/no`—Type (booleanp yes/no) .

Event macros may accept, among their inputs,
hints to prove applicability conditions.
These hints may be given by the user
either in the same form that follows `defthm`,
in which case the supplied hints are used
for all the applicability conditions,
or as a keyword-value list where each keyword identifies an applicability conditions
and the corresponding value consists of hints
(in the same form that follows `defthm`)
that are used for the identified applicability condition.

In the first case, the hints should be always a true list, based on the general form shown in the topic about computed hints, which further says that each element of the list may be either a common hint (see the topic about hints) or a computed hints. However, for now we do capture any constraints on these elements, and allow, in the definition of this recognizer, any true list for this first case of event macro hints.

In the second case of event macro hints, the values of the keyword-value list should be always true lists, as reasoned above for the first case. Similarly, we do not capture further constraints on the values. A keyword-value list is a bit like an alist from keywords to values, but it is more convenient to have an event macros's input processing turn that into an actual alist. Thus, this recognizer, which is for processed hints, recognizes alists from keywords to true lists for the second case of event macro hints.

So we would like to define this recognizer as the disjunction of
`true-listp` for the first case and
`keyword-truelist-alistp` for the second case.
However, since the latter implies the form
(i.e. an alist is a true list, as stated by the local theorem below),
the disjunction can be simplified to just `true-listp`.
Code that operates on values recognized by this predicate
can still do different things based on whether the values
satisfy `keyword-truelist-alistp` or just `true-listp`.

We prefer to introduce this explicit recognizer,
instead of using its current definiens `true-listp` directly,
so that (i) the intent is more clear
(i.e. it is not any true list; it is processed event macro hints)
and (ii) we may add further constraints in the future.

**Function: **

(defun evmac-input-hints-p (x) (declare (xargs :guard t)) (let ((__function__ 'evmac-input-hints-p)) (declare (ignorable __function__)) (true-listp x)))

**Theorem: **

(defthm booleanp-of-evmac-input-hints-p (b* ((yes/no (evmac-input-hints-p x))) (booleanp yes/no)) :rule-classes :rewrite)

**Theorem: **

(defthm evmac-input-hints-p-when-keyword-truelist-alistp (implies (keyword-truelist-alistp x) (evmac-input-hints-p x)))

**Theorem: **

(defthm evmac-input-hints-p-when-true-listp (implies (true-listp x) (evmac-input-hints-p x)))