Question regarding "Expected type"'s last line changing

Stream: general

[Crul]

Hi, this is my first message on zulip and I'm not sure if this is the appropriate place to ask a noob question. Please move or remove if this is not the right place.

The question is about why the last line of the "Expected type" message changes when you are inside a calc block.

I'm following this YouTube series about Lean and in the 6th chapter they use this very simple example.

import Mathlib.Tactic

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

I noticed that when you are in a line inside a 'calc' block: the last line changes from the goal "⊢ a = 2" to "⊢ ℤ".
I guess it's because the calc block only "needs" (<- not sure what the correct term is) that the result is an integer, because we've declared 'a' as an integer, and the "Expected type" shows the "subtype" (again, not sure the correct terms) of the 'calc' block. Is that right?

I posted the question on the YT video and they sent me here. Thanks for the help!

[Eric Paul]

It depends on where your cursor is inside the calc block.
Try putting your cursor at the very beginning of a line in the calc block and moving it to right and watch as the expected type changes.

[Crul]

@Eric Paul Yeah, I realized it changes in other places, but I preferred to keep the question simple.
Seeing what happens when I move the cursor reinforces my intuition that the "Expected type" depends on the context (closure?) but I would prefer to read a technical explanation and learn the proper terms so I can better search for help when needed.
Thanks.

[rzeta0]

I too am interested in this question.

[Kim Morrison]

I'm not sure what the question is, beyond what Eric Paul has already answered above. Could you clarify?

[Crul]

Probably I don't know enough to understand something that is very obvious for mathematicians; Eric Paul just said that "it depends on where the cursor is", which I already knew and that I should try moving the cursor, which I already did but I did not understand the underlying logic.

I'm not even sure I know enough to properly formulate the question, but I will give it another try:

• When you move the cursor, the [last line of the] "Expected type" message changes. What is the underlying logic to determine it?

Thanks!

[Damiano Testa]

In order for lean to successfully parse what you are writing, it should be type-correct. Whenever lean is expecting a specific type, since otherwise it knows that it will be a type error, it tells you what it expects at that point.

Does this help?

[Crul]

Kind-of ... I just realized that Lean is based on dependent type theory, which is something I still don't understand. So that explains why I'm so lost.

I will try again once I have some idea about dependent type theory.
Thanks again.