Finish Basics

[yurrriq]

• Introduction
• Enumerated Types
  • Edit first two paragraphs
  • Days of the Week
    • 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
    • Figure out how to redefine Nat locally, as in the Coq inner modules, Playground1 and Playground2.
      • plus
      • mult
      • minus
    • Verify the commentary on "wildcard pattern"
• 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.