Crafting a dependent typechecker, part 1
blueberrywren.dev