leanprover/tutorial — pull request #9 by avigad (2014-11-26 18:53:07+00:00)
Title: feat(02_Propositions_and_Proofs.org): add rough draft of second chapter

@soonhokong @leodemoura I assume that you automatically get these pull request. Let me know if not.

This is a rough draft of a second chapter. It is taking me longer than I thought; I only got as far as propositional logic. But I think it will work well as an introductory textbook. As always, feel free to edit and revise, and please let me know if you do not think I am heading in the right direction.

I think the next chapter, chapter 3, will look something like this:

3. Quantifiers and equality
The universal quantifier
Equality
The calc environment
The existential quantifier
The simplifier

Chapter 4 will cover inductive definitions and proofs by induction.