Zulip Chat Archive

Stream: new members

Topic: TPIL 3.7 labeled exercises


view this post on Zulip 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. :-)

view this post on Zulip 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: May 14 2021 at 12:18 UTC