Why the use of explicit type in (2:ℤ) ?

Stream: new members

[Hanson Char]

In the solution to Example 2.3.5 of The Mechanics of Proof, it explicitly specifies the type of 2 such as (2:ℤ) e.g.

      calc
        (2:ℤ) < 2 ^ 2 := by numbers

However, replacing all occurrences of (2:ℤ) by 2 also seems to work. So why the explicit type annotation? Could this be due to an older version of Lean4 where 2 defaulted to ℕ instead of ℤ, or the author chose to be explicit for pedagogical reasons?

[Kenny Lau]

it's good hygiene.

[Yaël Dillies]

One could ask Heather, but I suspect Hanson's putative explanation is spot on

[Kevin Buzzard]

But in today's lean 2 still defaults to Nat if no other clue is given, right?

[Kenny Lau]

Well you never know when lean chooses to interpret your 2 as N so I think it's better to just always specify

[Kenny Lau]

like yes it's not necessary here but that's what I mean by "good hygiene"

[Kenny Lau]

you're not guaranteed to catch a cold if you don't wash your hands once

[Hanson Char]

Kevin Buzzard said:

But in today's lean 2 still defaults to Nat if no other clue is given, right?

Are there good reasons to stay with Lean 2 or Lean 3 rather than moving on to Lean 4, besides perhaps the migration overhead?

[Kenny Lau]

@Hanson Char you misparsed the sentence. it says (in today's lean) ("2" still defaults ...)