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

Add LOC_BEFORE= in addition to LOC_AFTER=? #23

Open
david-a-wheeler opened this issue Jan 13, 2020 · 0 comments
Open

Add LOC_BEFORE= in addition to LOC_AFTER=? #23

david-a-wheeler opened this issue Jan 13, 2020 · 0 comments

Comments

@david-a-wheeler
Copy link
Contributor

Several places in the tutorial depend, in a fragile way, on the specific ordering of theorems in set.mm, because there's no way to say LOC_BEFORE=statement. You can only say LOC_AFTER=. But in all the tutorial cases, what you really want is to say "put this theorem BEFORE that one".

Could LOC_BEFORE=statement be added so that the tutorial would be more like to work over time?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant