From 320077f4a3096e49969a2ab6c1be1a387b01a5d8 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sat, 18 May 2024 20:51:53 +0900
Subject: [PATCH] =?UTF-8?q?=E3=80=8C=E4=BB=96=E3=81=AE=E5=A4=9A=E3=81=8F?=
 =?UTF-8?q?=E3=81=AE=E8=A8=80=E8=AA=9E=E3=80=8D=E3=81=8C=E6=9B=96=E6=98=A7?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

resolve #78
---
 Src/DependentType.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Src/DependentType.lean b/Src/DependentType.lean
index 58858db..bc38155 100644
--- a/Src/DependentType.lean
+++ b/Src/DependentType.lean
@@ -1,6 +1,6 @@
 /-
 # 依存型
-他の多くの言語ではできないのですが, Lean では型が値に依存することができます．これを**依存型**と呼びます．
+Lean では型が値に依存することができます．これを**依存型**と呼びます．他の言語でこれができるものとしては，Idris などがあります．
 
 これにより，たとえば関数 `f : A → B` の返り値の型が引数 `a : A` の値に依存することができ，そのような関数の型を `(a : A) → B` と書きます．これを特に**依存関数型**といいます．