Skip pattern synonyms + Warn about skipped definitions

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

Skip pattern synonyms + Warn about skipped definitions #168

Closed Lysxia closed 4 years ago

Lysxia commented 4 years ago

Related to #164. One day there should be some way of actually translating them, but just skipping them can already be helpful to handle some existing modules such as Data.Sequence.Internal in containers.

I also added some warnings because I got confused about whether I was doing something wrong when something wasn't getting translated, for example:

x, y :: ()
(x, y) = ((), ())

lastland commented 4 years ago

Looks like the CI is not happy because you added those warnings, and now the generated .v files do not match with those in the convenience copy. Can you try updating those and push them again?