macro コマンドと macro_rules コマンドの違い: macro コマンドは終わるまで syntax を導入しない

/- ## macro コマンドと macro_rules コマンドの違い
macro_rules コマンドは、展開の枝が一つしかなかったとしても、macro コマンドとは違っていて、
展開の右辺で左辺の宣言を使うことができる
-/
section

local syntax "my_repeat" tactic : tactic

local macro_rules
| `(tactic| my_repeat $t) => `(tactic| try ($t; my_repeat $t))

end

section

-- 右辺で宣言したばかりの `my_repeat` を使えない
-- macro コマンドが終わるまで syntax が登録されていないため
local macro "my_repeat" t:tactic : tactic => `(tactic| try $t; my_repeat $t)

end

Start from the Lean code example in the issue; no repository file or documentation section is specified. Determine where this explanation belongs, then ensure the documentation clearly explains when syntax becomes available for macro versus macro_rules and that the example is accurate.