		Search-engine friendly clone of the ACL2 documentation.

Evmac-input-hints-p

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 :hints in 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 :hints in 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.

Definitions and Theorems

Function: evmac-input-hints-p

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

Theorem: booleanp-of-evmac-input-hints-p

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

Theorem: evmac-input-hints-p-when-keyword-truelist-alistp

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

Theorem: evmac-input-hints-p-when-true-listp

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