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.