		Search-engine friendly clone of the ACL2 documentation.

Break-rewrite

Brr-near-missp

attachable function for determining “near misses”

This is a system function that determine whether a failed match of a monitored rule constitutes a near miss.

Note:This function is attachable (see defattach).

General Form:
(brr-near-missp msgp lemma target rcnst criteria-alist)

where msgp is t or nil, lemma is the ACL2 record representing a monitored :rewrite rule or :linear rule, target is a term to which the rewriter tried to apply the rule but failed to match the pattern in the lemma, rcnst is the rewrite constant at the time of the attempt, and criteria-alist is a symbol-alist associated with the rule in monitored-runes.

The function determines whether the pattern of the lemma “almost” matches the target, i.e., whether a “near miss” has occurred. The function is only called if the exact match failed. The built-in version of this function checks the criteria described in monitor. If a near miss has occurred, the result is either t or a message (see msg) object describing the near miss. If a near miss did not occur, the result is nil. See the source code for built-in-brr-near-missp for details of how the built-in version of this function operates.