[Typo] 2.9. Implicit Arguments: The makes -> The braces make #204
Description
Hi, I have finished (and much appreciated!) the book 3½ months ago, and compiled a little errata, which I would like to contribute. I am following the model indicated in the similar project for the book Functional Programming in Lean, but I understand that you might prefer this to be made in some other form: perhaps as a single issue, or even as a pull request. In that case, please let me know, and I will be most glad to help.
Here is the full quote for the first typo, which is highlighted in bold:
The makes the first argument to ident implicit.
Correction: The braces make