Simp Syntax

Stream: lean4

[Marcus Rossel]

I was looking at the syntax for the simp tactic and didn't understand one part:

syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic

What is the purpose of ,*,? - why not just ,*?
Also, since simpStar is within the ,*, simp allows some funny syntax:

example (a b : Nat) (h : b = c) : a + b = c + a := by
  simp [*, *, Nat.add_comm, *]

Should this actually throw an error, or is it just not important enough?

[Patrick Massot]

I think its goal is to allow a trailing comma.