hs-to-coq icon indicating copy to clipboard operation
hs-to-coq copied to clipboard

idea: people with experience write an index of module strategies

Open quinn-dougherty opened this issue 2 years ago • 0 comments

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 toward bytestring 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.

quinn-dougherty avatar Nov 02 '21 16:11 quinn-dougherty