An implementation of David Thrane Christiansen's language tartlet from Checking Dependent Types with Normalization by Evaluation: A Tutorial.
An implementation of David Thrane Christiansen's language tartlet from Checking Dependent Types with Normalization by Evaluation: A Tutorial.