> This seems like a spectacularly bad idea to me, but presumably it made somebody's awful hack work at one point. but elsewhere you say, "You are welcome to bu

> This seems like a spectacularly bad idea to me, but presumably it made somebody's awful hack work at one point. but elsewhere you say, "You are welcome to build a type which has this property and declares that it is Eq". This is exactly the difference between double and Double in Java. double has the `==` operator that isn't reflexive and works as required by IEEE-754 and Double has Double.equals, which is documented[1] to be a reflexive, transitive, symmetric, consistent, and substitutable relation. [1]: https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/lang/Object.html#equals(java.lang.Object) https://docs.oracle.com/en/java/javase/17/docs/api/java.base...