List.map の説明文の修正

Examples/Type/List.lean

@@ -59,15 +59,13 @@ end Hidden --#
 
 /- ## ファンクタとしての List
 
-`List` は `Functor` 型クラスのインスタンスになっています。
+`List` は `Functor` 型クラスのインスタンスになっており `<$>` 演算子が利用できます。
 -/
 
-#synth Functor List
+-- `<$>` 演算子が利用できる
+#guard (fun x => x * 2) <$> [1, 2, 3] = [2, 4, 6]
 
-/- つまり、`List` 型に包まれている要素に対して、関数を適用する高階関数 `List.map` を利用することができます。-/
+/- `f <$> xs` は `List` においては `List.map f xs` を表します。`List.map f xs` は、関数 `f : α → β` をリスト `xs : List α` の各要素に適用して新しく `List β` の項を作ります。このように「関数を引数に取る関数」なので `List.map` は高階関数と呼ばれることがあります。-/
 
 -- リストの各要素を 2 倍する
 #guard [1, 2, 3].map (fun x => x * 2) = [2, 4, 6]
-
--- `<$>` 演算子も利用できる
-#guard (fun x => x * 2) <$> [1, 2, 3] = [2, 4, 6]