Extend the command domain

Stream: Is there code for X?

[Asei Inoue]

import Lean

open Lean
/--- expand macro for 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}"

[Asei Inoue]

/-- expand macro for 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}"

[Asei Inoue]

These two commands do exactly the same thing, except for the syntax category of the arguments they receive. How can these be combined as one command?

[Asei Inoue]

This is my attempt:

import Lean

open Lean

syntax expandable := command <|> tactic

/-
invalid syntax node kind '«expandable#expand_»'
-/
elab "#expand " t:tactic : expandable => do
  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => logInfo m!"{t}"