diff --git a/Src/NamedArgument.lean b/Src/NamedArgument.lean new file mode 100644 index 0000000..5b5624d --- /dev/null +++ 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 index faa7403..0df4a82 100644 --- a/md/SUMMARY.md +++ b/md/SUMMARY.md @@ -21,4 +21,5 @@ * [コメント](./Comment.md) * [ドット記法](./build/DotNotation.md) -* [パイプライン演算子](./build/Pipeline.md) \ No newline at end of file +* [パイプライン演算子](./build/Pipeline.md) +* [名前付き引数](./build/NamedArgument.md) \ No newline at end of file