= 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).
== User's Guide ==
* [wiki:TypeNats/Basics Type-Level Naturals Basics]
* [wiki:TypeNats/Operations Type-Level Computation]
* [wiki:TypeNats/InductiveDefinitions Typed examinations of TNat (inductive definitions)]
== Notes on Design ==
* [wiki:TypeNats/AlternativeSingletons Alternative Design For Singletons]
* [wiki:TypeNats/AvoidingPartialTypeFunctions Avoiding Partial Type Functions]
== Notes on the Implementation ==
* [wiki:TypeNats/Implementation Implementation of GHC.TypeLits]
* [http://github.com/yav/tc-solver/blob/master/docs/axioms.md Axioms for type-level type operators]
== External links ==
* Where to find relevant source code:
* [http://darcs.haskell.org/cgi-bin/gitweb.cgi?p=ghc.git;a=shortlog;h=refs/heads/type-nats type-nats branch of GHC]
* libraries/base
* libraries/template-haskell
* utils/haddock
== XXX: Cleanup ==
* [wiki:TypeNats/Naturals Natural Numbers: From Values to Types]
* More advanced example: https://github.com/yav/memory-arrays/tree/master
* [wiki:TypeNats/Examples Examples]