match on sepBy/sepBy1

Stream: lean4

[Patrick Massot]

When I define some syntax using xs:term,* I can then match it with [$xs:term,*].  In the syntax description, xs:term,* is meant to be the abbreviation of sepBy(term, ","). Now say I want to use sepBy(term, "foo") or sepBy1(term, "foo"). How would I match that?

[Kyle Miller]

This appears to work:

syntax "bar " sepBy(term, "foo") : term

macro_rules
  | `(bar $[$ts]foo*) => `([$ts,*])

#check bar 1 foo 2 foo 3
-- [1, 2, 3] : List ℕ

[Patrick Massot]

Thanks!