Doubt in list type inference using #check

Stream: new members

[Ayush Agrawal]

I tried writing:

#check [1.1, 2, 3, 4.1]

I thought it should infer the list type as list R Real. However it is showing type list N

[11 / 10, 2, 3, 41 / 10] : list ℕ

Should't Lean refer it to type other than N?

[Anne Baanen]

By default, Lean will use ℕ for any numeric values. So also you should see:

#check 10 - 20 -- 10 - 20 : ℕ

On natural numbers, subtraction is defined to be saturating and division rounds down:

#eval 10 - 20 -- 0 : ℕ
#eval 11 / 10 -- 1 : ℕ

[Anne Baanen]

To get real numbers, you should be able to write:

import data.real.basic
#check [(1.1 : ℝ), 2, 3, 4.1]