Toy dependent typechecker using normalization by evaluation for fun and absolutely no profit. Based off of András Kovács' Elaboration Zoo - 03-holes and David Christiansen's tutorial, but using names instead of de Bruijn indices
Toy dependent typechecker using normalization by evaluation for fun and absolutely no profit. Based off of András Kovács' Elaboration Zoo - 03-holes and David Christiansen's tutorial, but using names instead of de Bruijn indices