You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Jan 5, 2025. It is now read-only.
Copy file name to clipboardExpand all lines: Manual/Monads/API.lean
+60-1Lines changed: 60 additions & 1 deletion
Original file line number
Diff line number
Diff line change
@@ -19,17 +19,36 @@ set_option pp.rawOnError true
19
19
20
20
set_option linter.unusedVariables false
21
21
22
+
/-
22
23
#doc (Manual) "API Reference" =>
24
+
-/
25
+
#doc (Manual) "API リファレンス(API Reference)" =>
23
26
27
+
:::comment
24
28
In addition to the general functions described here, there are some functions that are conventionally defined as part of the API of in the namespace of each collection type:
25
29
* `mapM` maps a monadic function.
26
30
* `forM` maps a monadic function, throwing away the result.
27
31
* `filterM` filters using a monadic predicate, returning the values that satisfy it.
28
32
29
33
30
-
::::example"Monadic Collection Operations"
34
+
:::
35
+
36
+
ここで説明する一般的な関数に加えて、各コレクション型の名前空間の API の一部として慣習的に定義されている関数がいくつかあります:
37
+
* `mapM` はモナド関数をマップします。
38
+
* `forM` はモナド関数をマップし、結果を捨てます。
39
+
* `filterM` はモナド述語を使ってフィルタリングを行い、それを満たす値を返します。
40
+
41
+
:::comment
42
+
::example"Monadic Collection Operations"
43
+
:::
44
+
::::example"モナドのコレクションに対する操作"
45
+
:::comment
31
46
{name}`Array.filterM` can be used to write a filter that depends on a side effect.
0 commit comments