Hints-specifier
Specifies the form of hints for an APT transformation.
The :hints keyword for an APT transformation is legal when there is
at least one applicability condition. The value may be a legal ACL2::hints value, that is, a legal value for the theorem prover's
:hints option, as provided for example in a defthm event.
Otherwise its value should be a keyword-value list (see keyword-value-listp)
(:KWD1 h1 :KWD2 h2 ...)
whose keywords KWDk are unique and include only names of
applicability conditions, where each value hk is a legal ACL2::hints value as discussed above.
Subtopics
- Ensure-is-hints-specifier
- Cause an error if a value is not a hints specifier.
- Canonical-hints-specifier-p
- Recognize canonical hints specifiers,i.e. hints specifiers that are
keyword-value-lists that associated applicability conditions with
hints.
- Canonicalize-hints-specifier
- Turn a hints specifier into an equivalent canonical one.
- Hints-specifier-p
- Recognize hints specifiers.
