import Lean

open Lean Elab Tactic

syntax "Foo" (ident <|> num) : tactic

elab_rules : tactic 
  | `(tactic| Foo $x:num) => 
    logInfo "num"

macro_rules 
  | `(tactic| Foo $x:ident) => `(tactic| trace "ident")

example : True := by 
  Foo x -- should not fail
  trivial