Enum Macro

Stream: lean4

[Joseph O]

Why can I not do this?

macro_rules
  | `(enum $id:ident { $[$ids:ident ,]* }) =>
    `(inductive $id where $[| $ids:ident]*)

error:

unexpected syntax
  inductive $id where$[
    | $ids:ident]*

expected command

[Marcus Rossel]

Did you define the enum-syntax before?

[Joseph O]

Marcus Rossel said:

Did you define the enum-syntax before?

Oh wait i think i forgot to change it

[Joseph O]

It works now

[Notification Bot]

Joseph O has marked this topic as resolved.

[Notification Bot]

Joseph O has marked this topic as unresolved.

[Joseph O]

Any way I can make this possible?

syntax "enum" ident "{" (ident ",")* ident "}" ";": command

macro_rules
  | `(enum $name:ident { $[$ids:ident ,]* $id:ident };) =>
    `(inductive $name where $[| $ids:ident]* | $id:ident)

[Joseph O]

Even better, make the last comma optional