Suggestion: add definitional floating point equality

Both Agda and Idris had unsoundness caused by using IEEE floating point equality as definitional equality, whereby `0.0 == -0.0` despite the two values being different and behaving differently. In particular, `1 / 0.0 = infinity` while `1 / -0.0 = -infinity`, breaking function congruence. See idris-lang/Idris-dev#2609 idris-lang/Idris2#601, agda/agda#2169