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.

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

More auto for lists #147

Open
awalterschulze opened this issue Jan 5, 2021 · 0 comments
Open

More auto for lists #147

awalterschulze opened this issue Jan 5, 2021 · 0 comments
Labels
enhancement New feature or request good first issue Good for newcomers

Comments

@awalterschulze
Copy link
Member

awalterschulze commented Jan 5, 2021

In chapter 13 of Coq Art, we see the use of the following tactic:

autorewrite with llists using auto with llists. 

I suspect this does more rewrites that just using autorewrite, but it would be good to investigate if this is better than auto with list or 'autorewrite with list` in CoqStock.

See
https://github.com/awalterschulze/regex-reexamined-coq/blob/master/src/CoqStock/List.v

See if examples are proven easier with this tactic or create proofs that are show that this tactic is superior in some way and add a comment explaining.

@awalterschulze awalterschulze added enhancement New feature or request good first issue Good for newcomers labels Jan 5, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request good first issue Good for newcomers
Projects
None yet
Development

No branches or pull requests

1 participant