latte-central / latte-kernel

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

Normalisation by evaluation 3 #12

Closed AustenPrinciple closed 4 years ago

AustenPrinciple commented 4 years ago

In norm.cljc, we can choose to use either the old beta-step, the new nbe, or both and alpha-compare the results. All tests pass obviously, but the time difference between the three options is negligible