[Agda] Nat arithmetic properties

Roman effectfully at gmail.com
Thu Sep 22 20:54:14 CEST 2016


Sergei, you seem to compute with records a lot, so I wonder: what will
happen if you try to type check your development with the
--no-eta-equality flag enabled? Or at least some part of it, if you
actually use eta-rules somewhere.
https://github.com/agda/agda/blob/14b9fbb11264a136f6b1e92373ee4a9149d006e4/CHANGELOG#L299


More information about the Agda mailing list