Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Better rewrite engine #124

Open
lastland opened this issue Nov 3, 2020 · 2 comments
Open

Better rewrite engine #124

lastland opened this issue Nov 3, 2020 · 2 comments

Comments

@lastland
Copy link
Collaborator

lastland commented Nov 3, 2020

Issue by antalsz
Thursday May 16, 2019 at 03:42 GMT
Originally opened as antalsz/hs-to-coq#124

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?
@lastland
Copy link
Collaborator Author

lastland commented Nov 3, 2020

Comment by antalsz
Thursday May 16, 2019 at 04:20 GMT

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

@lastland
Copy link
Collaborator Author

lastland commented Nov 3, 2020

Comment by antalsz
Thursday May 16, 2019 at 04:42 GMT

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@lastland