syntax/macro question

Stream: mathlib4

[Floris van Doorn]

Is there a way to do the following without introducing foo?

syntax foo := (ppSpace str)?
syntax (name := my_attribute) "my_attribute" foo : attr
macro "my_macro" x:foo : attr => `(attr| my_attribute $x)

I want to write something like x:(ppSpace str)?, but that is not accepted.

[Gabriel Ebner]

The type of x in x:(ppSpace str)? should give you a hint. :smile:

[Gabriel Ebner]

syntax (name := my_attribute) "my_attribute" (ppSpace str)? : attr
macro "my_macro" x:(ppSpace str)? : attr => `(attr| my_attribute $[$x]?)

[Floris van Doorn]

Thank you, that works.
To be honest, I don't really understand the $[$x]? or $[$y]* in syntax patterns like this. But I'm glad it works now :-)

[Henrik Böving]

We call it a splice it is described in the meta programming book github.com/arthurpaulino/lean4-metaprogramming-book/

If you know python it is a liiittle bit like a list comprehension. if $x is a list of syntax stuff you can use the $[$y]* to basically say "for all elements in the list of syntax objects y construct the syntax that is inside of the [] and the ? is similar but slightly different in the sense that $x is an optional thing so here the splice says "if it was passed do the thing in the [] otherwise skip it.