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.

[Albert Atserias]

I have some (small/minor) comments on Theorem Proving in Lean 4 here https://lean-lang.org/theorem_proving_in_lean4/ . Who should I send them to?

[Oliver Nash]

@Albert Atserias Depending on the comments, you could just open a PR to the repo: https://github.com/leanprover/theorem_proving_in_lean4