search

girving / interval

Conservative floating point interval arithmetic in Lean
Apache License 2.0
7 stars 1 forks source link

"Correct" pretty-printing of Interval #16

Closed adomasbaliuka closed 1 week ago

adomasbaliuka commented 2 weeks ago

The outside the interval thing is just broken printing: the underlying actual values will be fine. Originally posted by @girving in https://github.com/girving/interval/issues/7#issuecomment-2306768300

Are you already working on this, as you indicated you might?

I should have time to look at it next week, so in case you don't get around to it I might try.

girving commented 2 weeks ago

Yes, I’m already working on it. Maybe another week.

girving commented 1 week ago

Printing should be much better now. Let me know if it doesn't work!

adomasbaliuka commented 1 week ago

Thanks!

I saw you have some test in the code but no test directory. Are you in favor of adding one (regardless of whether it makes sense to move existing tests there or not)?

I'm thinking of adding some about the conversions and maybe some for the pretty printing would also be good?

girving commented 1 week ago

A test directory would be good! And +1 to moving existing tests there. It would be good to have no uses of native_decide outside of the test directory (at least initially).