parser allowing no tactics after by

Stream: lean4

[Floris van Doorn]

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 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

[Kevin Buzzard]

I have seen this "don't report the important error until much later than expected" phenomenon several times before, but it's only now that I understand what's going on! Certainly after the dot my muscle memory now immediately types sorry and this is probably why.

[Sebastian Ullrich]

This has been suggested before but this is a nice analysis of further issues. I'm not aware of any downsides, it just hasn't been done so far.

[Mario Carneiro]

Yes please! Other lists of 1 or more that should be 0 or more:

• 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

In most cases, the nullary case does nothing, but it should be a warning/error at elaboration time, not a parse error (since this generally results in degraded errors or spuriously grabbing the next token out of desperation)

[Kayla Thomas]

Is this related to needing to put sorry after the statement of a theorem before any errors in the way the theorem is stated are shown?

[Kayla Thomas]

And needing to go to the correct indentation before the next goal is shown?

[Kayla Thomas]

I guess yes on the first, maybe not on the second.