Stream: hs-to-coq devs & users

Topic: nonrecursive mode


view this post on Zulip Quinn (Oct 19 2021 at 03:28):

Moreover, has anyone reported back from the -N flag (leaving dependencies opaque)? I'm having trouble imagining how I would model stuff with opaque dependencies.

view this post on Zulip Stephanie Weirich (Oct 19 2021 at 13:02):

The use pattern for multi-module projects that we have explored is to translate each module using separate invocations of hs-to-coq. That way each module can be translated with its own set of edits (perhaps drawing from a shared edit file). Some of the makefiles for the larger examples (containers, ghc) demonstrate this structure. To translate a module abstractly, see the "axiomatize module" edit: https://hs-to-coq.readthedocs.io/en/latest/edits.html#axiomatize-module-replace-all-definitions-in-a-module-with-axioms


Last updated: Feb 06 2023 at 06:29 UTC