コマンド: macro_rules を紹介する

[Seasawher]

/-- 部分集合 -/
def Set (α : Type) := α → Prop

/-- 1つの要素だけからなる集合 -/
def Set.singleton (a : α) : Set α := fun x => x = a

/-- 集合に１つ要素を追加する -/
def Set.insert (a : α) (s : Set α) := fun x => x = a ∨ s x

-- 集合の波括弧記法の定義
-- 既存の記号と被らないようにするために二重にしている
syntax "{{" sepBy(term, ",") "}}" : term

-- まだ解釈方法を決めていないのでエラーになる
#check_failure {{2, 3}}

-- 集合の波括弧記法をどう解釈するのかのルール
macro_rules
  | `({{$x}}) => `(Set.singleton $x)
  | `({{$x, $xs:term,*}}) => `(Set.insert $x {{$xs,*}})

#check {{2, 3, 4, 5}}

[Seasawher]

macro_rules について

Lean Manual: https://lean-lang.org/lean4/doc/macro_overview.html?highlight=macro_rules#syntax-expansions-with-macro_rules-and-how-it-desugars

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: