Multiple commands from macro

Stream: lean4

[Henrik Böving]

I want to write a macro that lives in the command category and returns multiple commands, how can I get that? I tried using section to group the thing but that yields even weirder errors. MWE:

syntax "foo" : command
macro_rules
| `(command| foo) => `(command|
  inductive A : Type where | b : A
  def foo : Nat := 1
)
``

[Tomas Skrivan]

It works if you remove command| . Also there was some collision of using foo as identifier and command macro. So I turned the command to #foo

syntax "#foo" : command
macro_rules
| `(command| #foo) =>
 `(inductive A : Type where | b : A
   def foo : Nat := 1)

but don't ask me for an explanation :)

[Mac Malone]

@Henrik Böving To add on to Tomas's answer. command| only produces a single command syntax. multiple commands grouped together can be created via mkNullNode #[cmds](the basic `(...) quotation also has special magic to do this). section will not work because it does not actually group commands (section, the commands, and end are all actually separate commands).

[Mac Malone]

(mutual is the only builtin command block I know of that actually groups the commands inside it into a single overall mutual command)