Pledge tutorial
Pledge is a small language for learning restricted dependent types. This tutorial is a series of pages, each
with a task to solve in an editor that the type checker checks as you type. It needs JavaScript to run the
checker.
To read the lessons without JavaScript, follow a section's link to its source file, which holds
the text of its pages:
- First steps
- Types
that mention values
- Recursion
- Evidence
- Addition as a relation
- Arithmetic (optional)
- Limits and guarantees
- Erasure
- Appendix: fine points
Other pages: the editor,
the specification and
the repository.