term::= ...
|Applies a function inside a functor. This is used to overload the `<$>` operator.
When mapping a constant function, use `Functor.mapConst` instead, because it may be more
efficient.
Conventions for notations in identifiers:
* The recommended spelling of `<$>` in identifiers is `map`.term<$>term
term::= ...
|Maps a function over a functor, with parameters swapped so that the function comes last.
This function is `Functor.map` with the parameters reversed, typically used via the `<&>` operator.
Conventions for notations in identifiers:
* The recommended spelling of `<&>` in identifiers is `mapRev`.term<&>term
term::= ...
|The implementation of the `<*>` operator.
In a monad, `mf <*> mx` is the same as `do let f ← mf; x ← mx; pure (f x)`: it evaluates the
function first, then the argument, and applies one to the other.
To avoid surprising evaluation semantics, `mx` is taken "lazily", using a `Unit → f α` function.
Conventions for notations in identifiers:
* The recommended spelling of `<*>` in identifiers is `seq`.term<*>term
term::= ...
|Sequences the effects of two terms, discarding the value of the first. This function is usually
invoked via the `*>` operator.
Given `x : f α` and `y : f β`, `x *> y` runs `x`, then runs `y`, and finally returns the result of
`y`.
The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from `f`.
Conventions for notations in identifiers:
* The recommended spelling of `*>` in identifiers is `seqRight`.term*>term
term::= ...
|Sequences the effects of two terms, discarding the value of the second. This function is usually
invoked via the `<*` operator.
Given `x : f α` and `y : f β`, `x <* y` runs `x`, then runs `y`, and finally returns the result of
`x`.
The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from `f`.
Conventions for notations in identifiers:
* The recommended spelling of `<*` in identifiers is `seqLeft`.term<*term
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.
Conventions for notations in identifiers:
* The recommended spelling of `<|>` in identifiers is `orElse`.term<|>term
structureUserwherename:StringfavoriteNat:Natdefmain:IOUnit:=pure()Infix Functor and Applicative Operators
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 }
term::= ...
|Sequences two computations, allowing the second to depend on the value computed by the first.
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`.
Conventions for notations in identifiers:
* The recommended spelling of `>>=` in identifiers is `bind`.term>>=term
term::= ...
|Same as `Bind.bind` but with arguments swapped.
Conventions for notations in identifiers:
* The recommended spelling of `=<<` in identifiers is `bindLeft`.term=<<term
term::= ...
|Left-to-right composition of Kleisli arrows.
Conventions for notations in identifiers:
* The recommended spelling of `>=>` in identifiers is `kleisliRight`.term>=>term
term::= ...
|Right-to-left composition of Kleisli arrows.
Conventions for notations in identifiers:
* The recommended spelling of `<=<` in identifiers is `kleisliLeft`.term<=<term
Monad 主要通过 Lean.Parser.Term.do : termdo-notation 使用，这是一种用于命令式编程的嵌入式语言。
它提供了熟悉的语法来排序有效的操作、提前返回、局部可变变量、循环和异常处理。
所有这些功能都转换为 Monad 类型类的操作，其中一些功能需要添加指定容器迭代的类实例，例如 ForIn。
有关 Lean.Parser.Term.do : termdo 表示法设计的更多详细信息，请参阅 Ullrich and de Moura (2022)Sebastian Ullrich and Leonardo de Moura, 2022. “do Unchained: Embracing Local Imperativity in a Purely Functional Language”. In Proceedings of the ACM on Programming Languages: ICFP 2022.。
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 ()`.
returnterm
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 ()`.
return
并非所有 monad 都包含提前返回。
因此，当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() 的缩写。
当 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 项。
在 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 `Std.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 `Std.ToStream` typeclass.
in 循环允许对数据结构进行迭代。
循环体是包含 Lean.Parser.Term.do : termdo 块的一部分，因此可以使用局部效果，例如提前返回和可变变量。
syntaxIteration over Collections
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 `Std.ToStream` typeclass.
for((ident:)?terminterm),*dodoSeqItem*
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 `Std.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 `Std.ToStream` typeclass.
in 循环至少需要一个子句来指定要执行的迭代，该子句由一个可选的成员资格证明名称后跟一个冒号 (:)、一个要绑定的模式、关键字 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 `Std.ToStream` typeclass.
in 和一个集合术语组成。
该模式可能只是 identifier，必须与集合中的任何元素匹配；此位置的模式不能用作隐式过滤器。
可以通过用逗号分隔来提供进一步的子句。
每个集合都会同时迭代，当任何一个集合用完元素时，迭代就会停止。
Iteration over Array Indices with 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 `Std.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 `Std.ToStream` typeclass.
for 迭代数组的有效索引时，命名成员资格证明允许策略成功搜索数组索引在界限内的证明。
for 循环的迭代被转化为 ForIn.forIn 的使用，它是 ForM.forM 的类似物，增加了对局部突变和提前终止的支持。
ForIn.forIn 接收本地可变状态的初始值和一元操作作为参数，以及迭代的集合。
传递给 ForIn.forIn 的单子操作将当前状态作为参数，并在单子 m 中执行操作后，返回 ForInStep.yield 以指示迭代应使用一组更新的本地可变值继续，或者返回 ForInStep.done 以指示 Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break 或 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被执行。
迭代完成后，ForIn.forIn 返回局部可变值的最终值。
Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue 语句跳过最接近的封闭 Lean.doElemRepeat_repeat、Lean.doElemWhile_Do_while 或 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 `Std.ToStream` typeclass.
for 循环体的其余部分，继续进行下一次迭代。
Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break 语句终止最接近的封闭 Lean.doElemRepeat_repeat、Lean.doElemWhile_Do_while 或 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 `Std.ToStream` typeclass.
for 循环，从而停止迭代。
syntaxLoop Control Statements
doSeqItem::= ...
|`continue` skips to the next iteration of the surrounding `for` loop. continue
doSeqItem::= ...
|`break` exits the surrounding `for` loop. break
根据经验，这可以使用 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.doElemRepeat_repeat、Lean.doElemWhile_Do_while 和 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 `Std.ToStream` typeclass.
for 主体中的元素与包含它们的循环属于同一 Lean.Parser.Term.do : termdo 块。作为 Lean.doElemWhile_Do_while 和 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 `Std.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 `Std.ToStream` typeclass.
do 关键字不会引入新的 Lean.Parser.Term.do : termdo 块。
这是因为 Lean.Parser.Term.doIf : doElemif 下的 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.doIf : doElemif 属于同一 Lean.Parser.Term.do : termdo。
如果作为其他 Lean.Parser.Term.do : termdo 块中的元素出现的 Lean.Parser.Term.do : termdo 块改为创建新块，则该示例将输出 7。
要与没有成员资格证明的 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 `Std.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 `Std.ToStream` typeclass.
for 循环。
Monadic iteration in do-blocks, using the forxinxs notation.
The parameter m is the monad of the do-block in which iteration is performed, ρ is the type of
the collection being iterated over, and α is the type of elements.
Monadically iterates over the contents of a collection xs, with a local state b and the
possibility of early termination.
Because a do block supports local mutable bindings along with return, and break, the monadic
action passed to ForIn.forIn takes a starting state in addition to the current element of the
collection and returns an updated state together with an indication of whether iteration should
continue or terminate. If the action returns ForInStep.done, then ForIn.forIn should stop
iteration and return the updated state. If the action returns ForInStep.yield, then
ForIn.forIn should continue iterating if there are further elements, passing the updated state
to the action.
Monadic iteration in do-blocks with a membership proof, using the forh:xinxs notation.
The parameter m is the monad of the do-block in which iteration is performed, ρ is the type of
the collection being iterated over, α is the type of elements, and d is the specific membership
predicate to provide.
Monadically iterates over the contents of a collection xs, with a local state b and the
possibility of early termination. At each iteration, the body of the loop is provided with a proof
that the current element is in the collection.
Because a do block supports local mutable bindings along with return, and break, the monadic
action passed to ForIn'.forIn' takes a starting state in addition to the current element of the
collection with its membership proof. The action returns an updated state together with an
indication of whether iteration should continue or terminate. If the action returns
ForInStep.done, then ForIn'.forIn' should stop iteration and return the updated state. If the
action returns ForInStep.yield, then ForIn'.forIn' should continue iterating if there are
further elements, passing the updated state to the action.
An indication of whether a loop's body terminated early that's used to compile the forxinxs
notation.
A collection's ForIn or ForIn' instance describes how to iterate over its elements. The monadic
action that represents the body of the loop returns a ForInStepα, where α is the local state
used to implement features such as letmut.
Overloaded monadic iteration over some container type.
An instance of ForMmγα describes how to iterate a monadic operator over a container of type γ
with elements of type α in the monad m. The element type should be uniquely determined by the
monad and the container.
Use ForM.forIn to construct a ForIn instance from a ForM instance, thus enabling the use of
the for operator in do-notation.
