a typo in Theorem Proving in Lean 4

Stream: general

[Stepan Holub]

I believe, in Theorem Proving in Lean 4, there is a small but unpleasant (especially for the beginner at this stage) typo:

Incidentally, just as False has only an elimination rule, True has only an introduction rule, True.intro : true. In other words, True is simply true, and has a canonical proof, True.intro.

It should be True.intro : True (capital T).

(BTW, what is the preferred way for this kind of proof-reading message?)

[Kevin Buzzard]

Just make a PR to the book! It's at https://github.com/leanprover/theorem_proving_in_lean4 . They'll be grateful.

[Stepan Holub]

Done. Thanks.