search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Makeshift solution for deriving Eq #33

Closed sweirich closed 6 years ago

sweirich commented 7 years ago

Right now, everytime we do deriving Eq, we need to add 

redefine Local Definition instance_GHC_Base_Eq__Boxity_op_zsze__ : Boxity -> (Boxity -> bool) := fun arg_319__ arg_320__ =>  match arg_319__ , arg_320__ with | a , b => negb (instance_GHC_Base_Eq__Boxity_op_zeze__ a b)  end.

to the edits file.

Fixing this in a principled way is challenging. But for now, we can workaround by dropping /= from the Eq type class and defining /= as a separate function.

sweirich commented 6 years ago

Marking this as closed as we did it a long time ago.