RFC: Allow trailing comma after the last element of a list

[lenianiva]

Proposal

Currently this is not legal Lean:

let li = [
  item1,
  item2,
]

but if it were legal, adding new elements would not entail changes to existing lines:

let li = [
  item1,
  item2,
  item3,
  item4,
]

This has two main benefits:

1. Machine based code generation is simpler
2. The diff generated by version control is easier to read when new elements are added. This is especially relevant to unit testing.

Trailing comma is already supported in Rust and Python.

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

Discussion thread

James Gllicchio proposed that we could also have preceding commas:

let li = [
  , item1
  , item2
]

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[leodemoura]

@Kha I think this is a good change, and I recall discussing it with you in the past. However, I don't remember why we didn't move forward. I don't have time to do it myself, but I will support a PR. BTW, let's ensure the trailing comma is accepted in other similar notation.

[lenianiva]

@Kha I think this is a good change, and I recall discussing it with you in the past. However, I don't remember why we didn't move forward. I don't have time to do it myself, but I will support a PR. BTW, let's ensure the trailing comma is accepted in other similar notation.

What do you mean by accepted in other similar notation?

[kim-em]

e.g. if this is allowed, then rw [x, y, ] should be allowed as well.

[Kha]

However, I don't remember why we didn't move forward.

I am quite sure it was lack of sufficient motivation. So I agree with

I don't have time to do it myself, but I will support a PR.

[lenianiva]

@Kha I think this is a good change, and I recall discussing it with you in the past. However, I don't remember why we didn't move forward. I don't have time to do it myself, but I will support a PR. BTW, let's ensure the trailing comma is accepted in other similar notation.

I have a PR here #2643.

[leodemoura]

Closing this issue since PR #2643 has been merged.