counterexamples icon indicating copy to clipboard operation
counterexamples copied to clipboard

Published 20 hours ago • verified publisher icon stedolan

Suggestion: add definitional floating point equality

Open alercah opened this issue 1 year ago • 0 comments

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

alercah avatar Jun 07 '23 06:06 alercah