Recommended reading order:
- basic syntax
- reference to other definitions
- local bindings
- some syntax sugars
- unicode syntax example
- non-recursive sum: bool
- dependent product: pi type
- dependent coproduct: sigma type
- recursive sum: nat
- parametric recursive sum: maybe
- empty type and its eliminator
- universe levels
- subtyping for sums
- merging two sums
This script is used to run integration tests.