From 15448ae399661eed68088f5c8fbd202c97d7aa48 Mon Sep 17 00:00:00 2001
From: qiancy98 <49993496+qiancy98@users.noreply.github.com>
Date: Wed, 4 Sep 2024 15:34:33 +0800
Subject: [PATCH] Update quantifiers_and_equality.md
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

删掉多余字符`'`
---
 quantifiers_and_equality.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md
index 74b3223..b6da4b4 100644
--- a/quantifiers_and_equality.md
+++ b/quantifiers_and_equality.md
@@ -1131,7 +1131,7 @@ expression introduced in this way using the keyword ``this``:
 
 我们已经看到像 ``fun``、``have`` 和 ``show`` 这样的关键字使得写出反映非正式数学证明结构的正式证明项成为可能。在本节中，我们将讨论证明语言的一些通常很方便的附加特性。
 
-首先，我们可以使用匿名的 ``have`` 表达式来引入一个辅助目标，而不需要标注它。我们可以使用关键字 ``this``'来引用最后一个以这种方式引入的表达式:
+首先，我们可以使用匿名的 ``have`` 表达式来引入一个辅助目标，而不需要标注它。我们可以使用关键字 ``this`` 来引用最后一个以这种方式引入的表达式:
 
 ```lean
 variable (f : Nat → Nat)