| Chapter | Search & Replace | Adapt Text | Adapt Code | Review |
|---|---|---|---|---|
| preface | [x] | [ ] | [ ] | [ ] |
| basics | [x] | [ ] | [ ] | [ ] |
| induction | [x] | [ ] | [ ] | [ ] |
| lists | [x] | [ ] | [ ] | [ ] |
| poly | [x] | [ ] | [ ] | [ ] |
| tactics | [x] | [ ] | [ ] | [ ] |
| logic | [x] | [ ] | [ ] | [ ] |
| indprop | [x] | [ ] | [ ] | [ ] |
| maps | [x] | [ ] | [ ] | [ ] |
| proofobjects | [x] | [ ] | [ ] | [ ] |
| indprinciples | [x] | [ ] | [ ] | [ ] |
| rel | [x] | [ ] | [ ] | [ ] |
| imp | [x] | [ ] | [ ] | [ ] |
| impparser | [x] | [ ] | [ ] | [ ] |
| impcevalfun | [x] | [ ] | [ ] | [ ] |
| extraction | [x] | [ ] | [ ] | [ ] |
| auto | [x] | [ ] | [ ] | [ ] |
| postscript | [x] | [ ] | [ ] | [ ] |
| bib | [x] | [ ] | [ ] | [ ] |
-
Search & Replace: replace "Coq" and "Galina" with Lean;
-
Adapt Text: whenever Coq techniques differ from Lean techniques, replace for appropriate explanations. Specifically, universes, type classes, modules and tactics will be big sources of change;
-
Adapt Code: change Coq code for Lean code and ensure that it fits the new Lean explanations;
-
Review: read chapter from beginning to end, from end to beginning and do the exercises to make sure the whole is conherent.