syntax help

Stream: lean4

[Scott Morrison]

Sorry, I just can't remember the squiggles for decomposing Syntax. Can someone fill in this sorry:

import Lean

syntax forbidden := " [" ("-" ident,*,?) "]"

syntax "tac" (forbidden)? : tactic

open Lean Elab.Tactic Elab Tactic in
elab_rules : tactic |
    `(tactic| tac $[$forbidden]?) => do
      let forbidden : Array Name := sorry

[Alex J. Best]

Not sure if this is exactly what you want but

import Mathlib
import Lean

syntax forbidden := " [" ("-" ident,*,?) "]"

syntax "tac" (forbidden)? : tactic


open Lean Elab.Tactic Elab Tactic in
elab_rules : tactic |
    `(tactic| tac [ -$[$a],* ] ) => do
      let forbidden : Array Name :=
        a.map (Syntax.getId)
      logInfo (toString forbidden)

example : False := by
  tac [-a, b]

[Alex J. Best]

Alternative that may be more what you were trying to do originally

import Mathlib
import Lean

syntax forbidden := " [" (("-" ident),*,?) "]"

syntax "tac" (forbidden)? : tactic

open Lean Elab.Tactic Elab Tactic in
elab_rules : tactic |
    `(tactic| tac [ $[-$a],* ] ) => do
      let forbidden : Array Name :=
        a.map (Syntax.getId)
      logInfo (toString forbidden)

example : False := by
  tac [-a, -b]

[Scott Morrison]

Perfect, thank you @Alex J. Best.