# 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       |