Zulip Chat Archive

Stream: new members

Topic: TPIL 3.7 labeled exercises


Eduardo Cavazos (Oct 27 2019 at 10:52):

I've posted a few questions to stackoverflow around the proofs in exercise 3.7. It'd be nice to reference individual ones by exercise number, except that they aren't individually labeled.

In case the authors think it would be helpful, I've added a pull request which itemizes the proofs. So when discussing these a reader can say "I have a question about exercise 3.7.1.ii":

https://github.com/leanprover/theorem_proving_in_lean/blob/2d70939d2ced1b4f626b07d24b655e894fee0a22/propositions_and_proofs.rst

(Scroll to the very bottom to see how they're labeled.)

No worries if not accepted. Just a suggestion. :-)

Jeremy Avigad (Nov 13 2019 at 18:50):

@Eduardo Cavazos I am sorry that it took me so long to get to this. I did something slightly different: it looked better to number the identities in the preceding section, and I moved the "try me!" code block to the exercises. Thanks for your help, and for all the recent corrections.


Last updated: Dec 20 2023 at 11:08 UTC