Skip to content

Commit

Permalink
Fix rintros typo
Browse files Browse the repository at this point in the history
  • Loading branch information
PatrickMassot committed Jul 2, 2024
1 parent 3fa84e6 commit a42c260
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion MIL/C03_Logic/S02_The_Existential_Quantifier.lean
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,7 @@ Notice that the third proof begins by ``by``, after which the tactic version
of ``match`` expects a tactic proof on the right side of the arrow.
The last example is a proof term: there are no tactics in sight.
For the rest of this book, we will stick to ``rcases``, ``rintros``, and ``obtain``,
For the rest of this book, we will stick to ``rcases``, ``rintro``, and ``obtain``,
as the preferred ways of using an existential quantifier.
But it can't hurt to see the alternative syntax, especially if there is
a chance you will find yourself in the company of computer scientists.
Expand Down

0 comments on commit a42c260

Please sign in to comment.