Parsing then reassembling syntax

Stream: lean4

[Eric Wieser]

What am I doing wrong here?

syntax "test_sage_output" (&" only")? (" [" term,* "]")? term : tactic

syntax "create_sage_output_test" (&" only")? (" [" term,* "]")? : tactic

elab_rules : tactic
  | `(tactic| create_sage_output_test $[only%$onlyTk]? $[[$hypsStx,*]]?) => do
    let foo := `(tactic| test_sage_output $[only%$onlyTk]? $[[$hypsStx,*]]? sorry)
    sorry

I want foo to be exacty the same syntax but with the first token replaced and the sorry token appended

[Eric Wieser]

Is the syntax for pattern matching syntax different to the syntax for building syntax quotations?

[Eric Wieser]

And if so, is there a cheat-sheet for translating between one and the other?

[Sebastian Ullrich]

A syntax quotation term is a monadic value, you need to bind it