RFC: parser should allow empty (tactic) lists

[fpvandoorn]

After you write by or · (focus on 1 goal), you often look at the goal state for a while before deciding what tactic to apply next. It is annoying that these two pieces of syntax are illegal by themselves, since they require a nonempty sequence of tactics to follow. This has 2 negative consequences:

• A distracting parser error is shown
• Potential other errors are not shown

Suggestion: can the parser allow by or · (focus) followed by an empty sequence of tactics? The elaborator can still throw an warning/error of course.

The following MWE shows some examples of parser errors even though there is a "more important" error to show in both cases.

example (p : Prop) : p ∧ 3 := by

example (p q : Prop) : p ∧ q := by
  rw [doesntExist]
  constructor
  · 
  done

@digama0 also suggested that the parser allows an empty list in the following cases:

• def foo : type where
• mutual end
• variable
• universe
• export Foo ()
• open Foo ()
• open Foo hiding
• open Foo renaming
• open
• attribute [attr]
• do {}
• do
• if cond then <-- this one should probably be a warning, unindented code after if cond then is almost certainly a bug

Related RFC: #3556

Community Feedback

The Zulip thread shows a lot of support.

Impact

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

[Kha]

Potential problematic interaction: https://github.com/leanprover/lean4/pull/3215#issuecomment-1920888466