Normalisation by evaluation

latte-central / latte-kernel

The (very) small kernel of the LaTTe proof assistant

MIT License

11 stars 4 forks source link

Normalisation by evaluation #9

Closed AustenPrinciple closed 4 years ago

AustenPrinciple commented 4 years ago

NBE is fully set up, with quite a lot of tests. (of course all tests present are valid) The last steps would be to incorporate it into norm.cljc and benchmark it.

AustenPrinciple commented 4 years ago

In norm.cljc, it is not very clear as to where I should put my function nbe/norm, the functions beta-step, beta-red, and beta-normalize seem quite redundant.

fredokun commented 4 years ago

Look at the usage of the namespace norm in the typer ... It's not a problem to redefined both beta-red and beta-step (but I see the PR is closed).