renaming module does not combine mutual Inductives

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 6 years ago

sweirich commented 6 years ago

I was confused: we aren't producing a mutual inductive datatype for mutually recursive modules.

I've extended the tests/RenameModule test case to test this feature. Now currently fails.