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

[Typo] Exercise 2 in chapter 9 should be plusR_succ_left instead of plus_succ_left? #159

Open
spearman opened this issue Sep 15, 2024 · 1 comment
Labels
Typo Typographical or grammatical errors in the text

Comments

@spearman
Copy link

* Rewrite the proof of `plus_succ_left` to use `<;>` in a single line.

The exercise states:

  • Rewrite the proof of plus_succ_left to use <;> in a single line.

plus_succ_left doesn't appear anywhere else in the text, but plusR_succ_left does.

@spearman spearman added the Typo Typographical or grammatical errors in the text label Sep 15, 2024
@david-christiansen
Copy link
Collaborator

Thanks for the report! I'm knee-deep in work on the Lean reference manual, but an update to FPiL is planned for after that. I'll fix it then, if not before.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Typo Typographical or grammatical errors in the text
Projects
None yet
Development

No branches or pull requests

2 participants