15 lines
847 B
Markdown
15 lines
847 B
Markdown
|
# Typelevel
|
||
|
|
|
||
|
|
Experiments in the realm of typelevel Purescript computation.
|
||
|
|
|
||
|
|
## File structure
|
||
|
|
|
||
|
|
| File | Description |
|
||
|
|
| ------------------------------------ | -------------------------------------------------- |
|
||
|
|
| [Ast.purs](./src/Ast.purs) | Typelevel sum-types and a bit of typelevel parsing |
|
||
|
|
| [Num.purs](./src/Num.purs) | Typelevel naturals |
|
||
|
|
| [Vec.purs](./src/Vec.purs) | Typelevel fixed-size lists |
|
||
|
|
| [Ordering.purs](./src/Ordering.purs) | Typelevel orderings |
|
||
|
|
| [Term.purs](./src/Term.purs) | Typelevel lambda-calculus evaluation |
|
||
|
|
| [Fin.purs](./src/Fin.purs) | Bounded naturals using a GADT representation |
|