Conversation

Do you know of any programming languages that define NaN to be equal to itself?

Replying to

I'm pretty sure that in order to remain consistent, this needs to be the case in for definitional equality in dependently typed languages, although not necessarily for regular comparisons with `_==_`. See, for example: agda.readthedocs.io/en/v2.5.4.2/la

7:01 AM · Mar 14, 2022Twitter Web App

Replying to

and

IIRC there are a bunch of issues you can find about people finding inconsistencies in Idris and Agda due to floating point IEEE-754 comparisons being incompatible with definitional equality.