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

Published 20 hours ago • verified publisher icon antalsz

Better `rewrite` engine

Open antalsz opened this issue 5 years ago • 2 comments

Our rewrite engine is a bare-bones version of something more honest. For example, what about real support for variable binding, or handling nonlinear patterns gracefully?

antalsz avatar May 16 '19 03:05 antalsz

This also extends to improving the Coq parser, such as by supporting let 'pair x y := ... in ....

antalsz avatar May 16 '19 04:05 antalsz

And being consistent in where we apply rewrites – for instance, we don't currently rewrite all generated matches

antalsz avatar May 16 '19 04:05 antalsz