Skip to content

Commit

Permalink
Update quantifiers_and_equality.md
Browse files Browse the repository at this point in the history
删掉多余字符`'`
  • Loading branch information
qiancy98 committed Sep 4, 2024
1 parent afcbd63 commit 15448ae
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion quantifiers_and_equality.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit 15448ae

Please sign in to comment.