From 814d5fa73d3b7f4ec34cd13b3d9c0f5b6a6c5f08 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Mon, 12 May 2025 00:58:49 -0400 Subject: [PATCH] Update the README file --- README.md | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/README.md b/README.md index 16ea495..a7ceb45 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# Kripke-style untyped NbE in racket +# untyped NbE in racket [![status-badge](https://woodpecker.electriclam.com/api/badges/4/status.svg)](https://woodpecker.electriclam.com/repos/4) An implementation of normalization by evaluation loosely based on [A @@ -10,7 +10,3 @@ Since the implementation is untyped, the `normalize` function only 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 -untyped NbE composed with Coquand's algorithm.