leanprover/tutorial — pull request #11 by avigad (2014-12-15 03:22:41+00:00)
Title: feat(04_Interacting_with_Lean.org): add draft of chapter 4

It is not carefully proofread and still needs work, but it is a start.

I tried to cover the most fundamental aspects of interaction with Lean. I ran out of energy when writing about the parser, and there are probably things we should talk about under "setting options". Please let me know if you can think of other things I should add.

Also, let me know if you have suggestions about the markup I am using. I used "#+BEGIN_SRC text" for blocks that are not Lean code, but they still generate the "Try it Yourself" button. I also used "#+BEGIN_CENTER" for displaying web links, but maybe there is something else I should use.

This week I will spend time cleaning up name of theorems in the library, adding comments to headers, and updating the markdown directory files. After that I can revise some of the examples in this chapter.

I think the next two chapters should be

Chapter 5: Inductive Types
Enumerated Types
Option Type and Subtypes
Inductive Structures
nat
list
binary trees
countably branching trees
Inductive families

Chapter 6: Structuring Theories and Proofs
Structuring Long Proofs (proof ... qed, "visible", etc.)
Sections and Contexts
Using Tactics

I am not sure whether the function definition package should be described in Chapter 5 as we go, or whether it should be a separate chapter.

It just occurred to me that I should split the "Using the Library" section of this chapter into two, "Using the Library" and "Naming Conventions". I will do that later.