5.5 nat

Stream: general

[Danil Berestov]

Hi, Could anyone explain why 5.5 has type nat?
#check 5.5

11 / 2 : ℕ

[Anne Baanen]

Hi! I believe it is simply because numbers are interpreted as naturals by default, e.g. #check -10 causes an error because there is no - operator on ℕ. If you want e.g. the rational number, you can write (5.5 : ℚ).

(Thank you for moving your post to a new thread!)

[Danil Berestov]

thanks

[Kyle Miller]

My understanding is that since finite decimal representations are rational, Lean writes them as m / n where m and n are given in terms of the bit0 and bit1 definitions, which only depend on has_add and has_one. Then there's some defaulting mechanism where Lean will assume you meant natural numbers if the type is otherwise unspecified.

You can see the representation like so:

set_option pp.notation false
set_option pp.numerals false
#check 5.5

This gives

has_div.div (bit1 (bit1 (bit0 has_one.one))) (bit0 has_one.one) : nat

The has_div instance for natural numbers is floor division:

example : 5.5 = 5 := rfl