# Mini-TT samples

Recommended reading order:

+ [basic syntax](./basics/simple.minitt)
+ [reference to other definitions](./basics/reference.minitt)
+ [local bindings](./basics/local-binding.minitt)
+ [some syntax sugars](./basics/syntacic-sugar.minitt)
+ [unicode syntax example](./basics/unicode.minitt)
+ [non-recursive sum: bool](./sum-split/bool.minitt)
+ [dependent product: pi type](./dependent/function.minitt)
+ [dependent coproduct: sigma type](./dependent/sigma.minitt)
+ [recursive sum: nat](./sum-split/nat.minitt)
+ [parametric recursive sum: maybe](./sum-split/maybe.minitt)
+ [empty type and its eliminator](./sum-split/empty-eliminate.minitt)
+ [universe levels](./basics/univese.minitt)
+ [subtyping for sums](./first-class-sum/subtyping.minitt)
+ [merging two sums](./sum-split/merge.minitt)

[This script](test.pl) is used to run integration tests.