hs-to-coq
hs-to-coq copied to clipboard
idea: people with experience write an index of module strategies
I'm gathering that there's a diversity of tactics.
- Just codegen over the whole library, like
examples/containers
- axiomatize parts of it by hand, like
examples/wc
's strategy towardbytestring
re here - various stages of middle ground
- other strategies i'm not aware of
My guess is it would be high value for someone knowledgeable and experienced with the tool to quite briefly run through a list of packages from hackage
and jot down strategies they'd recommend. For example, a discussion of what it would take to hs-to-coq
lens
would be a good way of teaching advanced usage of the tool.