Matching commands

Matching commands are used to directly invoke the rewriting engine's term pattern matcher. They can be useful for figuring out exactly what subjects can be matched by a complex pattern.

match $\lbrace$[ number ]$\rbrace$ $\lbrace$in module :$\rbrace$ pattern <=? subject-term $\lbrace$such that condition$\rbrace$ .

Performs straightforward matching in the given module. This kind of matching is used by the engine for applying membership axioms. The result is a list of at most number matching substitutions such that the subject term matches the pattern and the substitution satisfies the optional condition (whose syntactic form is the same as the one of conditions for conditional equations and memberships; see Section 4.3). If the upper bound clause is omitted, infinity is assumed. For examples, see Section 4.9.

xmatch $\lbrace$[ number ]$\rbrace$ $\lbrace$in module :$\rbrace$ pattern <=? subject-term $\lbrace$such that condition$\rbrace$ .

Works similarly to the previous command, except that it performs matching with extension for those theories that need it (those including the assoc or iter attributes). If the subject term (after theory normalization) has a symbol $f$ from an extension theory on top, only a piece of the top theory layer with $f$ on top need be matched. This kind of matching is used by the engine for applying equations and rules in order to accurately simulate equivalence class rewriting. The result is a list of all matches satisfying the given condition. If only part of the subject was matched, that part is given. For examples, see Sections 4.8 and 4.9.