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

Create a way to axiomatize or skip top-level pattern bindings #104

Open antalsz opened 6 years ago

antalsz commented 6 years ago

As it stands, we always translate them in normal modules, and always throw an error in axiomatized modules

sweirich commented 5 years ago

f9b2a4650c6a5f9ccfc99fb1a139815eef707116 has a partial solution here. See PrelNames for an example.
We should do something a little more graceful than ignoring the patterns that cannot be translated though. Also, it doesn't work in conjunction with axiomatization.