latte-central / latte-kernel

The (very) small kernel of the LaTTe proof assistant
MIT License
11 stars 4 forks source link

Normalisation by evaluation 5 #16

Closed AustenPrinciple closed 4 years ago

AustenPrinciple commented 4 years ago

NBE is way cleaner now, and easier to understand. No more nbe-specific syntax, although it was useful on the way.