leanprover/tutorial — pull request #10 by avigad (2014-12-08 02:52:08+00:00)
Title: first draft of chapter 3

It needs work, but things are moving along.

In Chapter 2, I used lower-case letters "a b c" for propositions. This pushed me to use lower-case letters "p x" "r x y" for predicates and relations in Chapter 3. Let me know if you think I should switch to upper case, either in Chapter 3 only or in both Chapters 2 or 3.

At this stage, readers can start writing some nontrivial proofs. I think it is a good idea to provide information in Chapter 4 that will help them do that, with topics like these:

o setting Lean options (e.g. pp options)
o browsing the Lean library
o using the native interface (auto completion, etc.)
o defining notation
o more on modules and imports
o more on sections and contexts

Then in Chapter 5, we can cover inductive definitions, induction, recursion, and function definitions. Then maybe Chapter 6 should be about building theories, using tactics, writing long proofs, opaque vs. transparent definitions, etc., and Chapter 7 can start with algebraic structures and type classes.

Let me know what you think. Any input will be helpful.