minor
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful

This commit is contained in:
Yiyun Liu 2025-04-29 18:18:55 -04:00
parent 94ac3167b9
commit efbd7bbcd5

View file

@ -7,9 +7,9 @@ Evaluation](https://www.brics.dk/RS/03/40/BRICS-RS-03-40.pdf) and
[Abel's thesis on NbE](https://www.cse.chalmers.se/~abela/habil.pdf).
Since the implementation is untyped, the `normalize` function only
gives you $\beta$-normal forms. However, you can get a little bit of
$\beta\eta$-equivalence by invoking Coquand's algorithm (`η-eq?`) on
$\beta$-normal forms.
gives you β-normal forms. However, you can get a little bit of
βη-equivalence by invoking Coquand's algorithm (`η-eq?`) on
β-normal forms.
I'm hoping to expand the repository into a benchmark suite where I can
visualize the performance trade-off of type-directed NbE compared to