From efbd7bbcd5f6e94dfaeacbd9d44ec37d2f734cf2 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 29 Apr 2025 18:18:55 -0400 Subject: [PATCH] minor --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 5e617a5..16ea495 100644 --- a/README.md +++ b/README.md @@ -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