Open Seasawher opened 6 days ago
macro_rules について
macro_rules lets you declare expansions for a given Syntax element using a syntax similar to a match statement. The left-hand side of a match arm is a quotation (with a leading
| for categories other than term and command) in which users can specify the pattern they'd like to write an expansion for. The right-hand side returns a syntax quotation which is the output the user wants to expand to. A feature of Lean's macro system is that if there are multiple expansions for a particular match, Lean will try the most recently declared expansion first, and will retry with other matching expansions if the previous attempt failed. This is particularly useful for extending existing tactics.
The following example shows both the retry behavior, and the fact that macros declared using the shorthand macro syntax can still have additional expansions declared with macro_rules. This transitivity tactic is implemented such that it will work for either Nat.le or Nat.lt. The Nat.lt version was declared "most recently", so it will be tried first, but if it fails (for example, if the actual term in question is Nat.le) the next potential expansion will be tried: