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

Improve solutions in chapter 2 #240

Open
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

pitmonticone
Copy link
Contributor

@pitmonticone pitmonticone commented Sep 19, 2024

  • Make solutions more structured and readable
  • Make finishing tactics more explicit

These changes are mostly based on the feedback I received from participants of the Lean Tutorial in Vienna.

@avigad
Copy link
Owner

avigad commented Jan 6, 2025

I expect that we used apply here rather than exact because we just introduced apply and we wanted the reader to get used to it. We'll re-evaluate this PR when we make another proofreading pass through MIL.

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

Successfully merging this pull request may close these issues.

2 participants