search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.46k stars 388 forks source link

Floats aren't hashable #3650

Open alok opened 5 months ago

alok commented 5 months ago

They implement BEq, so making them so seems a small step. My intended use case is writing some basic numerical code and building out support there.

digama0 commented 5 months ago

They don't implement BEq lawfully, because they use the IEEE 754 definition of float equality. So you wouldn't be able to use them in a hashmap anyway.

Exposing a Hashable instance is not completely trivial because NaN payload bytes aren't allowed to leak without breaking the lean model of the type. It could be done if you clear the NaN payload, but perhaps this would be best exposed as a function to UInt64 anyway, and then you can implement this in user code.

alok commented 5 months ago

This is making me think of something like the rust libraries for floats that avoid nans by construction and using the numeral overloading to make it nice to use.