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.0
despite the two values being different and behaving differently. In particular,1 / 0.0 = infinity
while1 / -0.0 = -infinity
, breaking function congruence.See idris-lang/Idris-dev#2609 idris-lang/Idris2#601, agda/agda#2169