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