latte-central / latte-kernel

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

Nbe #23

Closed fredokun closed 4 years ago

fredokun commented 4 years ago

New normalization-by-evaluation scheme. Instead of the old (and now deprecated but still present) symbolic normalization scheme, the new scheme is more elegant. We let Clojure perform the beta-reductions instead of applying them by substitutions. Also, there is no a single pass for beta and delta reductions, hence the new scheme is faster, although not by a large margin.