「他の多くの言語」が曖昧

resolve #78
lean-ja · May 18, 2024 · 320077f · 320077f
1 parent 3afb40a
commit 320077f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Src/DependentType.lean b/Src/DependentType.lean
@@ -1,6 +1,6 @@
 /-
 # 依存型
-他の多くの言語ではできないのですが, Lean では型が値に依存することができます．これを**依存型**と呼びます．
+Lean では型が値に依存することができます．これを**依存型**と呼びます．他の言語でこれができるものとしては，Idris などがあります．
 
 これにより，たとえば関数 `f : A → B` の返り値の型が引数 `a : A` の値に依存することができ，そのような関数の型を `(a : A) → B` と書きます．これを特に**依存関数型**といいます．