|Version 35 (modified by diatchki, 3 years ago) (diff)|
Type Level Naturals
This page collects information on how to work with type-level natural numbers, as implemented in the Haskell compiler GHC (ticket #4385).
- Type-Level Naturals Basics
- Type-Level Computation
- Typed examinations of TNat (inductive definitions)
Notes on Design
Notes on the Implementation
- type-nats branch of GHC
- type-nats branch of the base library
- type nats branch of template-haskell
- Also, there is a type-nats branch for 'haddock'.