Finish Basics

[yurrriq]

• [x] Introduction
• [ ] Enumerated Types
  • [ ] Edit first two paragraphs
  • [ ] Days of the Week
    • [x] Verify that top-level type signatures are ~~optional~~ required and edit paragraph accordingly
    • [ ] Discuss interactive editor support
    • [ ] Reword "... after some simplification"
    • [ ] Verify the "main uses" claim
  • [ ] Booleans
    • [ ] Edit the syntax paragraph
  • [ ] Function types
    • [ ] Confirm the "function types" wording
  • [ ] Modules
    • [ ] Flesh out description of Idris's module system
    • [ ] Discuss namespaces
  • [ ] Numbers
    • [x] ~~Figure out how to redefine Nat locally, as in the Coq inner modules, Playground1 and Playground2.~~
      • [x] ~~plus~~
      • [x] ~~mult~~
      • [x] ~~minus~~
    • [ ] Verify the commentary on "wildcard pattern"
• [x] Proof by Simplification
• [ ] Proof by Rewriting
• [ ] Proof by Case Analysis
  • [ ] More on Notation (Optional)
  • [ ] Fixpoint and Structural Recursion (Optional)
• [ ] More Exercises

[yurrriq]

N.B. The todo list above is almost definitely outdated.