Fix a sentence

Lean-zh · Jul 17, 2024 · f58af7a · f58af7a
1 parent 6093aa6
commit f58af7a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/functional-programming-lean/src/type-classes/polymorphism.md b/functional-programming-lean/src/type-classes/polymorphism.md
@@ -67,8  67,8 @@ For now, ignore these parameters to `Type`.
 -->
 
 在这个输出信息中，实例本身被给予了 `inst` 这个名字。
-此外，`Type` 后面有一个 `u_1` ，这是 Lean
-目前，可以忽略这些Type的参数。
 此外，`Type` 后面有一个 `u_1` ，这里使用了目前尚未介绍的 Lean 的特性。
 我们可以暂时忽略这些 `Type` 的参数。
 
 <!--
 ## Defining Polymorphic Functions with Instance Implicits