import Bookshelf.Avigad.Chapter_2
import Bookshelf.Avigad.Chapter_3
import Bookshelf.Avigad.Chapter_4
import Bookshelf.Avigad.Chapter_5
import Bookshelf.Avigad.Chapter_7
import Bookshelf.Avigad.Chapter_8

/-! # Theorem Proving in Lean

## Avigad, Jeremy.

### Lean

* [Chapter 2: Dependent Type Theory](Bookshelf/Avigad/Chapter_2.html)
* [Chapter 3: Propositions and Proofs](Bookshelf/Avigad/Chapter_3.html)
* [Chapter 4: Quantifiers and Equality](Bookshelf/Avigad/Chapter_4.html)
* [Chapter 5: Tactics](Bookshelf/Avigad/Chapter_5.html)
* [Chapter 7: Inductive Types](Bookshelf/Avigad/Chapter_7.html)
* [Chapter 8: Induction and Recursion](Bookshelf/Avigad/Chapter_8.html)
-/