g <$> x は Functor.map g x の省略形です。
term ::= ...
| If `f : α → β` and `x : F α` then `f <$> x : F β`.
x <&> g は Functor.map g x の省略形です。
term ::= ... | term <&> term
8.3. 構文（Syntax）
Lean は関手・アプリカティブ関手・モナドを使ったプログラミングに対して特別な構文をサポートしています：
-
最も一般的な操作には中置演算子が用意されています。
-
Lean.Parser.Term.do : termdo記法 と呼ばれる組み込み言語により、モナドでプログラムを記述する際に命令構文を使用することができます。
8.3.1. 中置演算子（Infix Operators）
中置演算子は主に小さい式や、 Monad インスタンスが無い場合に便利です。
8.3.1.1. 関手（Functors）
Functor.map には2つの中置演算子があります。
syntaxFunctor Operators
8.3.1.2. アプリカティブ関手（Applicative Functors）
syntaxApplicative Operators
g <*> x は Seq.seq g (fun () => x) の省略形です。この関数は制御が引数に到達しない可能性があるため、評価を遅らせるために挿入されます。
term ::= ...
| If `mf : F (α → β)` and `mx : F α`, then `mf <*> mx : F β`.
In a monad this is the same as `do let f ← mf; x ← mx; pure (f x)`:
it evaluates first the function, then the argument, and applies one to the other.
To avoid surprising evaluation semantics, `mx` is taken "lazily", using a
`Unit → f α` function.
e1 *> e2 は SeqRight.seqRight e1 (fun () => e2) の省略形です。
term ::= ...
| If `x : F α` and `y : F β`, then `x *> y` evaluates `x`, then `y`,
and returns the result of `y`.
To avoid surprising evaluation semantics, `y` is taken "lazily", using a
`Unit → f β` function.
e1 <* e2 は SeqLeft.seqLeft e1 (fun () => e2) の省略形です。
term ::= ...
| If `x : F α` and `y : F β`, then `x <* y` evaluates `x`, then `y`,
and returns the result of `x`.
To avoid surprising evaluation semantics, `y` is taken "lazily", using a
`Unit → f β` function.
多くのアプリカティブ関手は Alternative 型クラスによる失敗と回復もサポートしています。このクラスも中置演算子を持っています。
syntaxAlternative Operators
e <|> e' は OrElse.orElse e (fun () => e') の省略形です。この関数は制御が引数に到達しない可能性があるため、評価を遅らせるために挿入されます。
term ::= ...
| `a <|> b` executes `a` and returns the result, unless it fails in which
case it executes and returns `b`. Because `b` is not always executed, it
is passed as a thunk so it can be forced only when needed.
The meaning of this notation is type-dependent. structure User where
name : String
favoriteNat : Nat
def main : IO Unit := pure ()
Functor と Applicative の中置演算子
一般的な関数型プログラミングにおいて作用のあるコンテキストで純粋関数を使用するには Functor.map と Seq.seq を経由して関数を適用することが一般的です。関数への一連の引数は <$> を使って適用され、それぞれの引数は <*> で区切られます。
以下の例では、 User.mk というコンストラクタが main の本体内でこのイディオムを使って適用されています。
def getName : IO String := do
IO.println "What is your name?"
return (← (← IO.getStdin).getLine).trimRight
partial def getFavoriteNat : IO Nat := do
IO.println "What is your favorite natural number?"
let line ← (← IO.getStdin).getLine
if let some n := line.trim.toNat? then
return n
else
IO.println "Let's try again."
getFavoriteNat
structure User where
name : String
favoriteNat : Nat
deriving Repr
def main : IO Unit := do
let user ← User.mk <$> getName <*> getFavoriteNat
IO.println (repr user)
以下の入力で実行すると：
stdinA. Lean UserNone42以下を出力します：
stdoutWhat is your name?What is your favorite natural number?Let's try again.What is your favorite natural number?{ name := "A. Lean User", favoriteNat := 42 }8.3.1.3. モナド（Monads）
モナドは主に Lean.Parser.Term.do : termdo 記法 によって使用されます。しかし、演算子を使ってモナドの計算を記述する方が便利な場合もあります。
syntaxMonad Operators
act >>= f は Bind.bind act f の省略形です。
term ::= ...
| If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the
result of executing `x` to get a value of type `α` and then passing it to `f`.
同様に、逆向きの演算子 f =<< act は Bind.bind act f の省略形です。
term ::= ...
| Same as `Bind.bind` but with arguments swapped.
Kleisli の合成演算子 Bind.kleisliRight と Bind.kleisliLeft にも中置演算子があります。
term ::= ...
| Left-to-right composition of Kleisli arrows. term ::= ...
| Right-to-left composition of Kleisli arrows.
8.3.2. do 記法（do-Notation）
モナドは主に Lean.Parser.Term.do : termdo 記法 （ Lean.Parser.Term.do : termdo-notation ）によって使用されます。これは作用を持つ操作の列・早期リターン・可変なローカル変数・ループ・例外処理のためのおなじみの構文を提供します。これらの機能はすべて Monad 型クラスの操作に変換され、そのうちのいくつかは ForIn のようなコンテナに対する反復を指定するクラスのインスタンスを追加する必要があります。 Lean.Parser.Term.do : termdo 項は、キーワード Lean.Parser.Term.do : termdo に続く Lean.Parser.Term.do : termdo 要素 （ Lean.Parser.Term.do : termdo item ）から構成されます。
syntax
term ::= ... | do doSeqItem*
Lean.Parser.Term.do : termdo の要素はセミコロンで区切ることができます；セミコロンを用いない場合は、それぞれの要素で行を分け、同じインデントにしなければなりません。
8.3.2.1. 逐次計算（Sequential Computations）
Lean.Parser.Term.do : termdo 要素 の1つの形式は項です。
syntax
doSeqItem ::= ... | term
要素の列に続く項は bind の使用に変換されます；特に、 do e1; es は e1 >>= fun () => do es に変換されます。
| 脱糖後 |
|---|---|
do
e1
es | e1 >>= fun () => do es |
項の計算結果には名前を付けることができ、後続のステップで使用することができます。これは Lean.Parser.Term.doLet : doElemlet を使って行います。
syntax
Lean.Parser.Term.do : termdo ブロック内でのモナドによる Lean.Parser.Term.doLet : doElemlet 束縛には2つの形式があります。1つ目は識別子を結果に束縛するもので、オプションで型注釈をつけることができます：
doSeqItem ::= ... | let ident(:term)? ← term
2番目はパターンを結果に束縛します。 | で始まるフォールバック句は、パターンが結果にマッチしなかった場合の動作を指定します。
doSeqItem ::= ... | let term ← term (| doSeq)?
この構文も bind の使用に変換されます。 do let x ← e1; es は e1 >>= fun x => do es に変換され、フォールバック句はデフォルトのパターンマッチに変換されます。 Lean.Parser.Term.doLet : doElemlet は ← の代わりに標準的な定義構文 := によって使用することもできます。この場合はモナドではなく純粋な定義を示します：
syntax
doSeqItem ::= ...
| let `letDecl` matches the body of a let declaration `let f x1 x2 := e`,
`let pat := e` (where `pat` is an arbitrary term) or `let f | pat1 => e1 | pat2 => e2 ...`
(a pattern matching declaration), except for the `let` keyword itself.
`let rec` declarations are not handled here.
do let x := e; es は let x := e; do es に変換されます。
| 脱糖後 |
|---|---|
do
let x ← e1
es | e1 >>= fun x =>
do es |
do
let some x ← e1?
| fallback
es | e1? >>= fun
| some x => do
es
| _ => fallback |
do
let x := e
es | let x := e
do es |
Lean.Parser.Term.do : termdo ブロック内では、← を前置演算子として使用することができます。これが適用された式は新しい変数に置き換えられ、現在のステップの直前に bind を使って束縛されます。これにより、作用のある計算を 記述する ことと、実際にその作用を 実行する ことの区別を維持したまま、純粋な値を期待する位置でモナドの作用も使用することができます。複数回出現する ← は左から右へ、内側から外側の順に処理されます。
| 脱糖後 |
|---|---|
do
f (← e1) (← e2)
es | do
let x ← e1
let y ← e2
f x y
es |
do
let x := g (← h (← e1))
es | do
let y ← e1
let z ← h y
let x := g z
es |
Lean.Parser.Term.do : termdo 記法は、データに依存する逐次計算のサポートに加えて、早期リターン・ローカルの可変状態・早期終了のループなど、さまざまな作用におけるローカルでの追加作用もサポートしています。これらの作用は、ローカルの脱糖ではなく、 モナド変換子 のような方法で Lean.Parser.Term.do : termdo ブロック全体の変換によって実装されています。
8.3.2.2. 早期リターン（Early Return）
早期リターンは与えられた値で直ちに計算を終了します。値は最も近い Lean.Parser.Term.do : termdo ブロックを含む Lean.Parser.Term.do : termdo ブロックから返されます；しかし、場合によっては最も近い do キーワードからではないこともあります。 Lean.Parser.Term.do : termdo ブロックの範囲を決定する規則は 専用の節 で説明されています。
syntax
doSeqItem ::= ...
| `return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
doSeqItem ::= ...
| `return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
全てのモナドが早期リターンを含むわけではありません。したがって、 Lean.Parser.Term.do : termdo ブロックに Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return が含まれている場合、そのコードはその作用をシミュレートするために書き換えられる必要があります。モナド m の α 型の値を計算するために早期リターンを使用するプログラムは、 ExceptT α m α モナドのプログラムと考えることができます：早期リターンされる値は例外の経路を取り、通常の返却ではそちらを通りません。そして外部のハンドラはどちらのコードパスからも値を返すことができます。内部的には Lean.Parser.Term.do : termdo エラボレータはこのような変換を行います。
Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return だけ書かれた場合は、 Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return() の省略形です。
8.3.2.3. ローカルの可変状態（Local Mutable State）
ローカルの可変状態とは、それが定義されている Lean.Parser.Term.do : termdo ブロックからエスケープできないもののことです。 Lean.Parser.Term.doLet : doElemlet mut 束縛子はローカルの可変な束縛を導入します。
syntax
可変な束縛は、純粋な計算とモナドの計算のどちらでも初期化することができます：
doSeqItem ::= ... | let mut(ident |`letDecl` matches the body of a let declaration `let f x1 x2 := e`, `let pat := e` (where `pat` is an arbitrary term) or `let f | pat1 => e1 | pat2 => e2 ...` (a pattern matching declaration), except for the `let` keyword itself. `let rec` declarations are not handled here.hole ):= termA *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).
doSeqItem ::= ... | let mut ident ← doElem
同様に、純粋な値とモナドの計算結果のどちらでもミューテーションさせることができます：
doElem ::= ... | ident(: term)? := term
doElem ::= ... | term(: term)? := term
doElem ::= ... | ident(: term)? ← term
doElem ::= ... | term ← term (| doSeq)?
このようなローカルの可変な束縛は、そのレキシカルスコープの外では可変ではないため、 状態モナド よりも強力ではありません；この性質によって推論も簡単になります。 Lean.Parser.Term.do : termdo ブロックに可変な束縛が含まれている場合、 Lean.Parser.Term.do : termdo エラボレータは StateT と同じように式を変換し、新しいモナドを構築して正しい値で初期化します。
8.3.2.4. 制御構造（Control Structures）
Lean.Parser.Term.do : termdo 要素は Lean のほとんどの項レベルの制御構造に対応しています。これらは Lean.Parser.Term.do : termdo ブロックのステップとして出現する場合、項ではなく Lean.Parser.Term.do : termdo 要素として解釈されます。制御構造の各分岐は項ではなく Lean.Parser.Term.do : termdo 要素の列であり、それらのいくつかは対応する項よりも構文的に柔軟です。
syntax
構文上、 Lean.Parser.Term.doIf : doElemthen 分岐を省略することはできません。このような場合、 Lean.Parser.Term.doUnless : doElemunless は条件が偽の時にのみ本体を実行します。 Lean.Parser.Term.do : termdo 内の Lean.Parser.Term.doUnless : doElemunless は構文の一部であり、 Lean.Parser.Term.do : termdo の入れ子を誘導しません。
syntax
doSeqItem ::= ... | unless term do doSeqItem*
Lean.Parser.Term.doMatch : doElemmatch が Lean.Parser.Term.do : termdo ブロック内で使用されている場合、各分岐は同じブロックの一部と見なされます。そうでない場合。 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 項と同等です。
syntax
doSeqItem ::= ...
| match (`matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
`match h1 : e1, e2, h3 : e3 with ...`. 8.3.2.5. 反復処理（Iteration）
Lean.Parser.Term.do : termdo ブロック内では、 Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
for…Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
in ループによってデータ構造に対する反復処理を可能にします。ループの本体は Lean.Parser.Term.do : termdo ブロックを含むため、早期リターンや可変変数などのローカルの作用を使用することができます。
syntax
doSeqItem ::= ...
| `for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
for…Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
in ループでは、実行する反復処理を指定する句が少なくとも1つ必要です。この節は、コロン（:）が続くオプションのメンバシップ証明名・束縛パターン・キーワード Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
in ・コレクションの項から構成されます。パターンは 識別子 であり、コレクションの任意の要素と一致しなければなりません；この位置でのパターンは暗黙のフィルタとして使うことはできません。カンマで区切ることでさらに句を指定することができます。各コレクションは同時に反復され、いずれかのコレクションの要素がなくなると反復処理が停止します。
複数のコレクションに対する反復処理
複数のコレクションに対して反復処理する場合、いずれかのコレクションの要素がなくなると反復処理が停止します。
#eval Id.run do
let mut v := #[]
for x in [0:43], y in ['a', 'b'] do
v := v.push (x, y)
return v
#[(0, 'a'), (1, 'b')]
Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
for によるインデックスを用いた配列の繰り返し
Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
for で配列の有効なインデックスを反復処理する場合、メンバシップ証明に名前を付けることで配列のインデックスが範囲内にあることの証明を検索するタクティクが成功するようになります。
def satisfyingIndices (p : α → Prop) [DecidablePred p] (xs : Array α) : Array Nat := Id.run do
let mut out := #[]
for h : i in [0:xs.size] do
if p xs[i] then out := out.push i
return out
仮定名を省略すると、反復変数が指定された範囲内にあることを証明するものがコンテキストにないため、配列の検索に失敗します。
Lean.doElemWhile_Do_ : doElemwhile ループでは条件が真である限り本体が繰り返されます。 Lean.Parser.Command.declaration : commandpartial とマークされていない関数の中で、このループを使って無限ループを書くことができます。これは Lean.Parser.Command.declaration : commandpartial 修飾子が、定義されている関数によって引き起こされる非停止や無限後退にのみ適用され、その関数が呼び出す関数には適用されないためです。 Lean.doElemWhile_Do_ : doElemwhile ループの翻訳は別の補助関数に依存しています。
syntax
doSeqItem ::= ... | while term do doSeqItem*
doSeqItem ::= ... | while ident : term do doSeqItem*
Lean.doElemRepeat_ : doElemrepeat ループの本体は Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break 文が実行されるまで繰り返されます。 Lean.doElemWhile_Do_ : doElemwhile ループと同様に、これらのループは Lean.Parser.Command.declaration : commandpartial とマークされていない関数で使用することができます。
syntax
doSeqItem ::= ... | repeat doSeqItem*
Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue 文は最も近い Lean.doElemRepeat_ : doElemrepeat ・ Lean.doElemWhile_Do_ : doElemwhile ・ Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
for ループの本体の残りをスキップし、次の繰り返しに移ります。 Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break 文は最も近い Lean.doElemRepeat_ : doElemrepeat ・ Lean.doElemWhile_Do_ : doElemwhile ・ Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
for ループを終了し、反復を停止します。
syntax
doSeqItem ::= ...
| `continue` skips to the next iteration of the surrounding `for` loop. doSeqItem ::= ...
| `break` exits the surrounding `for` loop.
Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break に加えて、ループは常に現在のモナド内の作用によって終了させることができます。ループから例外を投げるとループが終了します。
8.3.2.6. do ブロックの識別（Identifying do Blocks）
Lean.Parser.Term.do : termdo 記法の多くの機能は 現在の Lean.Parser.Term.do : termdo ブロック （current Lean.Parser.Term.do : termdo block）に影響を与えます。特に、早期リターンは現在のブロックを中断させ、返却値で評価を行います。また可変な束縛はそれが定義されているブロックでのみミューテーションできます。これらの機能を理解するためには「同じ」ブロック内にあることの意味を正確に定義する必要があります。
経験的に、これは Lean 言語サーバを使って確認することができます。カーソルが Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return 文の上にある場合、対応する Lean.Parser.Term.do : termdo キーワードがハイライトされます。同じ Lean.Parser.Term.do : termdo ブロックの外側で可変な束縛をミューテーションしようとするとエラーメッセージが表示されます。
Lean.Parser.Term.do : termdoこの規則は以下に従います：
-
あるブロックを開始する
Lean.Parser.Term.do : termdoキーワードのすぐ下に入れ子になっている各要素は、そのブロックに属します。 -
ある
Lean.Parser.Term.do : termdoブロックの要素であるLean.Parser.Term.do : termdoキーワードのすぐ下に入れ子になっている各要素は。外側のブロックに属します。 -
Lean.Parser.Term.doIf : doElemif・Lean.Parser.Term.doMatch : doElemmatch・Lean.Parser.Term.doUnless : doElemunlessの分岐内の要素は、その要素を含んでいる制御構造と同じLean.Parser.Term.do : termdoブロックに属します。Lean.Parser.Term.doUnless : doElemunlessの構文の一部としてのLean.Parser.Term.doUnless : doElemdoキーワードは新しいLean.Parser.Term.do : termdoブロックを導入しません。 -
Lean.doElemRepeat_ : doElemrepeat・Lean.doElemWhile_Do_ : doElemwhile・Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `ToStream` typeclass.forの本体内の要素は、それらを含むループと同じLean.Parser.Term.do : termdoブロックに属します。Lean.doElemWhile_Do_ : doElemwhileとLean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `ToStream` typeclass.forの構文の一部としてのLean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `ToStream` typeclass.doキーワードは新しいLean.Parser.Term.do : termdoブロックを導入しません。
入れ子になった do と分岐
以下の例は 7 ではなく 6 を出力します：
def test : StateM Nat Unit := do
set 5
if true then
set 6
do return
set 7
return
#eval test.run 0
((), 6)
これは Lean.Parser.Term.doReturn : doElem`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
return 文が Lean.Parser.Term.doIf : doElemif の直下の Lean.Parser.Term.do : termdo と同じ Lean.Parser.Term.doIf : doElemif に属しているからです。この代わりに他の Lean.Parser.Term.do : termdo ブロックの要素として出現した Lean.Parser.Term.do : termdo ブロックによって新しいブロックを作成した場合、この例は 7 を出力します。
8.3.2.7. 反復処理のための型クラス（Type Classes for Iteration）
メンバシップ証明のない Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
for ループを使用するには、コレクションは ForIn 型クラスを実装している必要があります。 ForIn' を実装することで、さらにメンバシップ証明付きの Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
for ループを使用することができます。
type class
ForIn.{u, v, u₁, u₂} (m : Type u₁ → Type u₂)
(ρ : Type u) (α : outParam (Type v))
: Type (max (max (max u (u₁ + 1)) u₂) v)
ForIn m ρ α is the typeclass which supports for x in xs notation.
Here xs : ρ is the type of the collection to iterate over, x : α
is the element type which is made available inside the loop, and m is the monad
for the encompassing do block.
Instance Constructor
ForIn.mk.{u, v, u₁, u₂}
Methods
forIn : {β : Type u₁} → [inst : Monad m] → ρ → β → (α → β → m (ForInStep β)) → m β
forIn x b f : m β runs a for-loop in the monad m with additional state β.
This traverses over the "contents" of x, and passes the elements a : α to
f : α → β → m (ForInStep β). b : β is the initial state, and the return value
of f is the new state as well as a directive .done or .yield
which indicates whether to abort early or continue iteration.
The expression
let mut b := ... for x in xs do b ← foo x b
in a do block is syntactic sugar for:
let b := ... let b ← forIn xs b (fun x b => do let b ← foo x b return .yield b)
(Here b corresponds to the variables mutated in the loop.)
type class
ForIn'.{u, v, u₁, u₂} (m : Type u₁ → Type u₂)
(ρ : Type u) (α : outParam (Type v))
(d : outParam (Membership α ρ))
: Type (max (max (max u (u₁ + 1)) u₂) v)
ForIn' m ρ α d is a variation on the ForIn m ρ α typeclass which supports the
for h : x in xs notation. It is the same as for x in xs except that h : x ∈ xs
is provided as an additional argument to the body of the for-loop.
Instance Constructor
ForIn'.mk.{u, v, u₁, u₂}
Methods
forIn' : {β : Type u₁} → [inst : Monad m] → (x : ρ) → β → ((a : α) → a ∈ x → β → m (ForInStep β)) → m β
forIn' x b f : m β runs a for-loop in the monad m with additional state β.
This traverses over the "contents" of x, and passes the elements a : α along
with a proof that a ∈ x to f : (a : α) → a ∈ x → β → m (ForInStep β).
b : β is the initial state, and the return value
of f is the new state as well as a directive .done or .yield
which indicates whether to abort early or continue iteration.
inductive type
ForInStep.{u} (α : Type u) : Type u
Auxiliary type used to compile for x in xs notation.
This is the return value of the body of a ForIn call,
representing the body of a for loop. It can be:
-
.yield (a : α), meaning that we should continue the loop andais the new state..yieldis produced bycontinueand reaching the bottom of the loop body. -
.done (a : α), meaning that we should early-exit the loop with statea..doneis produced by calls tobreakorreturnin the loop,
Constructors
done.{u} {α : Type u} : α → ForInStep α
.done a means that we should early-exit the loop.
.done is produced by calls to break or return in the loop.
yield.{u} {α : Type u} : α → ForInStep α
.yield a means that we should continue the loop.
.yield is produced by continue and reaching the bottom of the loop body.
type class
ForM.{u, v, w₁, w₂} (m : Type u → Type v)
(γ : Type w₁) (α : outParam (Type w₂))
: Type (max (max (max (u + 1) v) w₁) w₂)
Typeclass for the polymorphic forM operation described in the "do unchained" paper.
Remark:
-
γis a "container" type of elements of typeα. -
αis treated as an output parameter by the typeclass resolution procedure. That is, it tries to find an instance using onlymandγ.
Instance Constructor
ForM.mk.{u, v, w₁, w₂}
Methods
forM : [inst : Monad m] → γ → (α → m PUnit) → m PUnit