| ... | ... | @@ -9,10 +9,15 @@ This page collects information on how to work with type-level natural numbers, a |
|
|
|
- [Natural Numbers: From Values to Types](type-nats/naturals)
|
|
|
|
- [Type-Level Operations](type-nats/operations)
|
|
|
|
|
|
|
|
## Implementation and Design Issues
|
|
|
|
## Notes on Design
|
|
|
|
|
|
|
|
- [Implementation of GHC.TypeNats](type-nats/implementation)
|
|
|
|
- [Alternative Design For Singletons](type-nats/alternative-singletons)
|
|
|
|
- [Avoiding Partial Type Functions](type-nats/avoiding-partial-type-functions)
|
|
|
|
- Naturals or Integers?
|
|
|
|
|
|
|
|
## Notes on the Implementation
|
|
|
|
|
|
|
|
- [Implementation of GHC.TypeNats](type-nats/implementation)
|
|
|
|
- [Axioms for Natural Number Operators](type-nats/axioms)
|
|
|
|
- GHC Interaction Rules ([Notational Conventions](type-nats/rule-notation))
|
|
|
|
|
| ... | ... | @@ -22,5 +27,10 @@ This page collects information on how to work with type-level natural numbers, a |
|
|
|
|
|
|
|
## External links
|
|
|
|
|
|
|
|
- [ Source repos](http://code.galois.com/darcs/type-naturals/)
|
|
|
|
- The implementation resides in several repositories:
|
|
|
|
|
|
|
|
- (GIT) Changes to GHC are on branch type-nats in: [ git://code.galois.com/type-naturals/ghc.git](git://code.galois.com/type-naturals/ghc.git)
|
|
|
|
- (DARCS) Changes to the base library are at [ http://code.galois.com/darcs/type-naturals/09-Jan-2011/base/](http://code.galois.com/darcs/type-naturals/09-Jan-2011/base/)
|
|
|
|
- (DARCS) Changes to the template-haskell library are at [ http://code.galois.com/darcs/type-naturals/09-Jan-2011/template-haskell/](http://code.galois.com/darcs/type-naturals/09-Jan-2011/template-haskell/)
|
|
|
|
|
|
|
|
- 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 |
