Skip to content
This repository was archived by the owner on Nov 17, 2020. It is now read-only.

Better rewrite engine #124

Open
antalsz opened this issue May 16, 2019 · 2 comments
Open

Better rewrite engine #124

antalsz opened this issue May 16, 2019 · 2 comments

Comments

@antalsz
Copy link
Owner

antalsz commented May 16, 2019

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
Copy link
Owner Author

antalsz commented May 16, 2019

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

@antalsz
Copy link
Owner Author

antalsz commented May 16, 2019

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

@lastland lastland mentioned this issue Nov 3, 2020
Open
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@antalsz