don't remove asserts from GHC

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

Closed sweirich closed 5 years ago

sweirich commented 6 years ago

Currently we remove GHC's asserts using edits (i.e. debugIsOn). Let's not, so that we can prove them.

sweirich commented 5 years ago

We can prove (most of) them. See cad3a4fd88be7d996e4417b7c7a8a2329d792d22. There weren't that many.