type-nats.md

@@ -3,10 +3,16 @@
 
 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)).
 
+## User's Guide
+
 - [Type-Level Naturals Basics](type-nats/basics)
 - [Simple Examples of Using GHC.TypeNats](type-nats/basic-examples)
-- [Implementation of GHC.TypeNats](type-nats/implementation)
 - [Design Notes about Nat vs. TypeNat](type-nats/implicit-explicit)
+
+## Implementation and Design Issues
+
+- [Implementation of {{{GHC.TypeNats}}}](type-nats/implementation)
+
 - [Axioms for Natural Number Operators](type-nats/axioms)
 - GHC Interaction Rules ([Notational Conventions](type-nats/rule-notation))
 
@@ -14,8 +20,7 @@ This page collects information on how to work with type-level natural numbers, a
   - [Simple Inert Interactions](type-nats/interact2)
   - [Solving (\<=) Predicates](type-nats/leq)
 
-
-External links:
+## External links
 
 - [ Source repos](http://code.galois.com/darcs/type-naturals/)
 - More advanced example: [ https://github.com/yav/memory-arrays/tree/master](https://github.com/yav/memory-arrays/tree/master)
\ No newline at end of file