From 396201245bf244f9d78e9007a02dd1c388193d27 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki+gh@protonmail.com>
Date: Thu, 2 Nov 2023 22:43:42 -0400
Subject: [PATCH] fix: typo in binder (#14)

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 20afb08..e9a15cc 100644
--- a/README.md
+++ b/README.md
@@ -165,7 +165,7 @@ because `α` is not a type.
   Maybe something like this:
 ```lean
 def turnExistsIntoForall : Q(Prop) → MetaM Q(Prop)
-  | ~q(∃ x, p x) => do
+  | ~q(∃ x, $p x) => do
      q(∀ x, $(x => turnExistsIntoForall q($p $x)))
   | e => e
 ```