understanding `calc` with 2 similar examples

Stream: new members

[rzeta0]

The following is a simple proof that seems valid:

example {a b : ℤ} (h1 : a = b + 1) (h2: b - 1 = 0) : a = 2 :=
  have h3:
    b = 1 := by linarith [h2]
  calc
    a = b + 1 := by rw [h1]
    _ = 1 + 1 := by rw [h3]
    _ = 2 := by norm_num

And the following is exactly the same but with an additional calc inside have h3:. This program also seems to be valid.

example {a b : ℤ} (h1 : a = b + 1) (h2: b - 1 = 0) : a = 2 :=
  have h3:
   calc   -- <-- ******** only difference ********
      b = 1 := by linarith [h2]
  calc
    a = b + 1 := by rw [h1]
    _ = 1 + 1 := by rw [h3]
    _ = 2 := by norm_num

I'm trying to understand calc at a deeper level than my initial introduction to it.

What is the difference between these two programs?

What does the extra calc in the second program actually do?

You may say it does nothing, that is, the syntax is valid but it is immediately overwritten by some new "mode" (I don't know what a mode is).

[Ruben Van de Velde]

calc with only one line doesn't work well

[Ruben Van de Velde]

But that's not the issue, calc doesn't make any sense in that position

[Yaël Dillies]

  have h3 :=
   calc   -- <-- ******** only difference ********
      b = 1 := by linarith [h2]

would make sense, however (well, maybe with an extra equation in)

[Ruben Van de Velde]

In have h : ty := t, h is the name of the statement you're proving, ty is the statement, and t is the proof. What would it mean to put calc in ty?

[rzeta0]

So the initial replies suggest it is wrong to put calc there - because there is no calculation to be done.

Is my confusion due to Lean not issuing a warning or error?

[Ruben Van de Velde]

There's an error unexpected end of input; expected ':=' at the end, but it's not very visible

[Kevin Buzzard]

If you get into the habit of ending proofs with done (which is great if you're experimenting like this) then you'll see the error much more clearly

[rzeta0]

Yhanks - i've done an internet search and can't find anything about done, and it isn't in the Heather Macbeth course thus far.

Any pointers to documentation would be gratefully received.

[Damiano Testa]

Hovering over done you should be able to see its doc-string.

[Damiano Testa]

E.g., try with

example : True := by exact .intro; done