自前で infixl コマンドを作る（マクロを作るマクロの例）

import Lean

open Lean

/-
  `infixl` を自前で定義する
  標準の `infixl` は `notation` に展開されるけど、習ったばかりの `$$x` の記法を使いたいので `macro` に展開する

  my_infixl:60 " ⊕ " => fun l r => (!l && r) || (l && !r)
  が
  macro l:term:60 " ⊕ " r:term:61 : term => `(fun l r => (!l && r) || (l && !r)) $l $r)
  に展開されるようにする
-/

syntax "my_infixl" (":" num)? str " => " term : command
macro_rules
| `(my_infixl $[: $precOpt]? $op => $f) =>
  let precL : TSyntax `num := precOpt.getD (Syntax.mkNumLit "60")
  let precR : TSyntax `num := quote <| precL.getNat + 1
  `(macro l:term:$precL $op:str r:term:$precR : term => `($f $$l $$r))

my_infixl:60 " ⊕ " => fun l r => (!l && r) || (l && !r)

#eval true ⊕ true
#eval true ⊕ false

/-- コマンドをマクロ展開するコマンド -/
elab "#expand_command " t:command : command => do
  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => logInfo m!"{t}"

/-- info: macro l✝:term✝:60 " ⊕ " r✝:term✝:61 : term✝ => `(lxor $l✝ $r✝) -/
#guard_msgs in
  #expand_command my_infixl:60 " ⊕ " => lxor

Start with the supplied Lean snippet, focusing on the syntax, macro_rules, and #expand_command entry points. Check the repository's existing code-example structure before deciding where this example belongs. Done means the self-contained my_infixl example is incorporated in the appropriate place and its shown #eval and #guard_msgs checks pass.