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.