inequalities with different types

Stream: general

[Colleen Robles]

Is there any documentation/guidence on inequalities between two different types? Specifically I have an integer (n : N) and a real number (x : R), and I want to compare them (eg, n < x). Lean seems to object to the discrepancy between types, and I've found that (n : R) < x does work. Is this the right way to go about it? And how does Lean "think" of (n : R)?

[Yaël Dillies]

Yes absolutely. There's in general no meaningful way to compare elements of different types. Here it makes sense because a natural is also a real, which Lean knows about by inserting the coercion coe : ℕ → ℝ when you type (n : ℝ) < x. The expression Lean creates is coe n < x, which makes sense.

[Yury G. Kudryashov]

One technical detail: Lean 3 inserts coe, Lean 4 unfolds the instance and inserts the function behind it; in this case, it is Nat.cast.