Toy implementation of Insanely Dependent Types
Features
- Insane pi-types:
[x1 : A1, x2 : A2, .., xn : An] -> B
All xi are in scope in the Ai's (and in B of course). Applications of
insane functions must be fully applied.
- Everything is mutually recursive
- Simple Agda-like syntax
Limitations
- No implicit arguments
- Function types and Set are not terms
- No indexed datatypes