Hi. I was going though the Ready, Set, Verify! paper.
In it, with regard to converting coq code back to haskell including the type class constraints, it's mentioned that
By providing an interface that restores the type- class based types, we can run the original containers test suite against this code
Is this interface openly available? To see how this was done?
It's probably here in the repository https://github.com/plclub/hs-to-coq/tree/master/examples/containers
Last updated: Feb 06 2023 at 06:29 UTC