Single line calc syntax

Stream: lean4

[Patrick Massot]

For beginners, it helps a bit to end each proof with done so that error don’t leak to the next declaration. When creating calc with the calc code action in mathlib (or the upcoming calc?), it helps to have single line calc as a temporary input. But those two things do not interact nicely. Consider the following #mwe (yes, I really mean no import).

example (a b : Int) (hb : b = 2) : a + a*b = 3*a := by
  calc a + a * b = 3 * a := by sorry
  done

Note that

example (a b : Int) (hb : b = 2) : a + a*b = 3*a := by
  calc
    a + a * b = 3 * a := by sorry
  done

also fails, but adding a second calc line works fine.

[Aaron Liu]

This is because calc takes its first line as "arbitrary indent, with optional :=". I think it would be beneficial to change this to "either arbitrary indent without :=, or strict indent with :=".

[Aaron Liu]

Zero-line calc is also kind of broken, and always elaborates as rfl, even when the relation is not =:

import Mathlib

/-
'calc' expression has type
  x = x : Prop
but is expected to have type
  x ⤳ x : Prop
-/
example {X : Type*} [TopologicalSpace X] {x : X} : x ⤳ x := calc x

[Patrick Massot]

I think the zero-line case is much less important.