Educational implementation of dependent types, with some extra things
Based on:
Löh, A., McBride, C., & Swierstra, W. (2010). A tutorial implementation of a dependently typed lambda calculus. Fundamenta informaticae, 102(2), 177-207.
with some experiments in extensible syntax.