Suggestion: add definitional floating point equality

[alercah]

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