Functor への言及をリンクにする

lean-ja · Nov 5, 2024 · 742c3cf · 742c3cf
1 parent 709646a
commit 742c3cf
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/LeanByExample/Reference/Diagnostic/Whnf.lean b/LeanByExample/Reference/Diagnostic/Whnf.lean
@@ -62,7 +62,7 @@ instance instMonadMany : Monad Many where
   pure := Many.one
   bind := Many.bind
 
-/- `Monad` 型クラスは `Functor` クラスや `Applicative` クラスの実装を含むので、`Many` は `Functor` や `Applicative` のインスタンスでもあります。このインスタンスは次のように `inferInstance` という関数で構成することができますが、その中身を `#print` で出力してみても実装がわかりません。-/
+/- `Monad` 型クラスは [`Functor`](#{root}/Reference/TypeClass/Functor.md) クラスや `Applicative` クラスの実装を含むので、`Many` は `Functor` や `Applicative` のインスタンスでもあります。このインスタンスは次のように `inferInstance` という関数で構成することができますが、その中身を `#print` で出力してみても実装がわかりません。-/
 
 def instManyFunctor : Functor Many := inferInstance
 

diff --git a/LeanByExample/Reference/Type/List.lean b/LeanByExample/Reference/Type/List.lean
@@ -63,7 +63,7 @@ end Hidden --#
 
 ### map
 
-`List` は `Functor` 型クラスのインスタンスになっているため `<$>` 演算子が利用できます。
+`List` は [`Functor`](#{root}/Reference/TypeClass/Functor.md) 型クラスのインスタンスになっているため `<$>` 演算子が利用できます。
 -/
 
 -- `<$>` 演算子が利用できる
-Original file line number
+Diff line change
@@ Expand Up / @@ -63,7 +63,7 @@ end Hidden --# @@
     ### map
-    `List` は `Functor` 型クラスのインスタンスになっているため `<$>` 演算子が利用できます。
+    `List` は [`Functor`](#{root}/Reference/TypeClass/Functor.md) 型クラスのインスタンスになっているため `<$>` 演算子が利用できます。
     -/
     -- `<$>` 演算子が利用できる
@@ Expand Down @@