Confused about result of float to int32 conversion

Stream: new members

[mdioc]

Hey everyone. I have been playing around with Lean for Advent of Code just to learn more about Lean in general but ran into something a bit confusing. I am sure its probably just a lack of knowledge from my part. I have a simplistic example:

#eval 39.000.toInt32 -- outputs 39 as I would expect
#eval (((50239.0 / 100.0) - 502.39.floor) * 100.0).toInt32 -- outputs 38 but the part before .toInt32 will output 39.0000

Is 38 actually what is expected in this case? I am confused a bit since I expect this to have the same result as the first example

[One Happy Fellow]

I think you are getting tripped up by floating point arithmetic here and not lean, see this in python:

>>> ((50239.0/100.0 - int(502.39)) * 100)
38.999999999998636

It is ever so slightly less than 39, so floor operation rounds it down.

[mdioc]

One Happy Fellow said:

I think you are getting tripped up by floating point arithmetic here and not lean, see this in python:

>>> ((50239.0/100.0 - int(502.39)) * 100)
38.999999999998636

It is ever so slightly less than 39, so floor operation rounds it down.

Yep I do indeed seem to be tripped up by the floating point math. Does #eval do some form of rounding for output?

I guess I was confused more by the fact that:

#eval ((50239.0 / 100.0) - 502.39.floor) * 100.0 -- outputs 39.000000

but your example does show the culprit :)

[Aaron Liu]

it's docs#Float.toString that's rounding

[mdioc]

Excellent, thanks both!