variable visibility in `theorem` vs `def`(book example)

Stream: new members

[Brandon Moore]

Just starting out, I installed in vscode according to the quickstart and created a "standalone" project. Writing and editing other example code in the Basic.lean file has worked fine, but the calc example from https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs fails:

variable (h1 : a = b)
variable (h2 : b = c + 1)
variable (h3 : c = d)
variable (h4 : e = 1 + d)

theorem T : a = e :=
  calc
    a = b      := h1
    _ = c + 1  := h2
    _ = d + 1  := congrArg Nat.succ h3
    _ = 1 + d  := Nat.add_comm d 1
    _ = e      := Eq.symm h4

it complains like unknown identifier 'b' for every variable mentioned in the body except a and e.

It does seem to work if theorem T is changed to def T or to example.

I guess it makes some sense if the variables become arguments after the section is closed, and the type of the theorem isn't supposed to depend on what is written in the body?

It seems this was a breaking change in 4.11: https://lean-lang.org/doc/reference/latest/releases/v4.11.0

How up to date are the examples in "Theorem Proving in Lean 4" supposed to be

[Yaël Dillies]

See #new members > A basic question about calc without tactics for a fix

[Yaël Dillies]

Examples are supposed to be up to date. You should probably open an issue, if none exists already