Cast Int to Real

Stream: new members

[Tomaz Gomes]

Hi, why isn't Real.intCast.intCast 0 definitionally equal to 0 : Real? For instance, if I do:

import Mathlib.Data.Real.Basic

example : (0 : ℚ) = Rat.ofInt (Int.ofNat 0) := rfl -- ok

example : (0 : ℝ) = Real.intCast.intCast 0 := rfl -- type mismatch on rfl

Is there another casting function that won't have this problem?

[Kevin Buzzard]

Why do you care about such implementation details? We have tactics which deal with all of this such as norm_cast.

[Tomaz Gomes]

I am implementing my own tactic, which involves casting variables from Int to Real. I will perform some operations on these variables, and I got some errors by assuming the equality I described. Also, I am curious about this :)

[Eric Wieser]

The reason they're not defeq is that we deliberately marked them as irreducible_def so that lean is not allowed to know that secretly they're defeq after all