|
|
|
# Type Level Naturals
|
|
|
|
# Type Level Literals
|
|
|
|
|
|
|
|
|
|
|
|
This page collects information on how to work with type-level natural numbers, as implemented in the Haskell compiler GHC (ticket [\#4385](https://gitlab.haskell.org//ghc/ghc/issues/4385)).
|
|
|
|
This page collects information on how to work with type-level literals, as implemented in the Haskell compiler GHC (ticket [\#4385](https://gitlab.haskell.org//ghc/ghc/issues/4385)).
|
|
|
|
|
|
|
|
## User's Guide
|
|
|
|
|
|
|
|
- [Type-Level Naturals Basics](type-nats/basics)
|
|
|
|
- [Type-Level Literal Basics](type-nats/basics)
|
|
|
|
- [Type-Level Computation](type-nats/operations)
|
|
|
|
- [Typed examinations of TNat (inductive definitions)](type-nats/inductive-definitions)
|
|
|
|
|
| ... | ... | |
