[orlp]

Python's floating point flooring division operator also has a pitfall: it gives a correctly rounded result as if you computed (a / b) with infinite precision before flooring. This can lead to the following:

    >>> 1 / 0.1
    10.0
    >>> 1 // 0.1
    9.0

This is because 0.1 is in actuality the floating point value value 0.1000000000000000055511151231257827021181583404541015625, and thus 1 divided by it is ever so slightly smaller than 10. Nevertheless, fpround(1 / fpround(1 / 10)) = 10 exactly.

I found out about this recently because in Polars I defined a // b for floats to be (a / b).floor(), which does return 10 for this computation. Since Python's correctly-rounded division is rather expensive, I chose to stick to this (more context: https://github.com/pola-rs/polars/issues/14596#issuecomment-...).