名前付き引数を追加

lean-ja · Mar 29, 2024 · 234d412 · 234d412
1 parent 6d23aaa
commit 234d412
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 1 deletion.
diff --git a/Src/NamedArgument.lean b/Src/NamedArgument.lean
@@ -0,0 +1,13 @@
+/-
+# 名前付き引数
+Lean では，関数に引数を渡すときに順序ではなく名前で引数を指定することができます．
+-/
+
+-- `foldl` には `init` という名前の引数がある
+#check List.foldl
+
+-- 本来は最初の引数は関数だが，
+#eval [1, 2, 3, 4].foldl (· + ·) 0
+
+-- 名前付き引数を使うと，引数の順序を変えることができる
+#eval [1, 2, 3, 4].foldl (init := 0) (· + ·)
diff --git a/md/SUMMARY.md b/md/SUMMARY.md
@@ -21,4 +21,5 @@
 
 * [コメント](./Comment.md)
 * [ドット記法](./build/DotNotation.md)
-* [パイプライン演算子](./build/Pipeline.md)
+* [パイプライン演算子](./build/Pipeline.md)
+* [名前付き引数](./build/NamedArgument.md)