I want to handle tactic and commands in a unified way

Stream: lean4

[Asei Inoue]

import Lean

def lxor (l r : Bool) : Bool := !l && r

open Lean

/-- command to expand macro of `command` -/
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}"

/-- command to expand macro of `tactic` -/
elab "#expand_tactic " t:tactic : command => do
  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => logInfo m!"{t}"

/-- syntax category for `#expand` -/
declare_syntax_cat macro_stx
syntax command : macro_stx
syntax tactic : macro_stx

-- this works!
/-- info: notation:50 lhs✝:51 " LXOR " rhs✝:51 => lxor lhs✝ rhs✝ -/
#guard_msgs in
  #expand_command infix:50 " LXOR " => lxor

syntax "#expand" macro_stx : command

-- new command for both tactic and command
elab "#expand " t:macro_stx : command => do
  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => logInfo m!"{t}"

-- This does not work....
-- why???
/-
Not a macro
-/
#expand infix:50 " LXOR " => lxor