name complex syntax match

Stream: lean4

[Thomas Murrills]

Basic question that I can't quickly find the answer to, but:

let's say I'm matching some syntax which includes

| `( ... $[ with $as,*]? ... )

I'd like to give a name to the piece of syntax with $as,* so that I can (e.g.) check if it .isSome. I know if it's a simple literal like !, I can say $[!%$h]?. Is there an analogue for more complex syntax, or a way I can group the complex syntax before %, without modifying the existing syntax definition I'm matching?

[Gabriel Ebner]

You should be able to do with%$tk

[Gabriel Ebner]

What type does as have? I thought it was an option.

[Thomas Murrills]

Oh, that should be enough in this case, thanks.

I was wondering, though, if in general (for other cases, since I've run into this more than once) there's a way to name the whole thing (here "with $as,*"), or if this is intentionally something we can't do.

[Sebastian Ullrich]

If it's something that makes sense to talk about as a whole, it should be its own syntax foo := ... declaration so that you can use an antiquotation $f:foo for it