ending of Data.Int.Cast.Defs

Stream: mathlib4

[Matthew Ballard]

Why does this file end with open Nat?

[Ruben Van de Velde]

There used to be some more code after it: https://github.com/leanprover-community/mathlib/blob/master/src/data/int/cast/defs.lean#L62

[Damiano Testa]

My guess is that the extra code may have become a syntactic tautology, or whatever it is called.

[Matthew Ballard]

#6710