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

Wrap together rw or simp tactics. #15

Open
faenuccio opened this issue Aug 25, 2023 · 0 comments
Open

Wrap together rw or simp tactics. #15

faenuccio opened this issue Aug 25, 2023 · 0 comments
Assignees
Labels
feature Something new should be implemented

Comments

@faenuccio
Copy link

Goal

I would like a command that wraps together several lines where the same tactic (accepting a list) is called with just one term, creating the corresponding list. While looking for a proof, one might add one thing at a time, but then wants everything to be more compact.

Example:

rw [foo1]
rw [foo2]
rw [foo3]

How to achieve

Example:

rw [foo1, foo2, foo3]

@faenuccio faenuccio added the bug Something isn't working label Aug 25, 2023
@DenisGorbachev DenisGorbachev added feature Something new should be implemented and removed bug Something isn't working labels Aug 25, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature Something new should be implemented
Projects
None yet
Development

No branches or pull requests

2 participants