Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Finish Basics #1

Open
7 of 27 tasks
yurrriq opened this issue Jun 27, 2016 · 1 comment
Open
7 of 27 tasks

Finish Basics #1

yurrriq opened this issue Jun 27, 2016 · 1 comment

Comments

@yurrriq
Copy link
Collaborator

yurrriq commented Jun 27, 2016

  • 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 yurrriq added this to the First ten chapters milestone Aug 3, 2017
@yurrriq
Copy link
Collaborator Author

yurrriq commented Aug 3, 2017

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant