Lean supports programming with functors, applicative functors, and monads via special syntax:
Infix operators are provided for the most common operations.
An embedded language called Lean.Parser.Term.do : termdo-notation allows the use of imperative syntax when writing programs in a monad.
Infix operators are primarily useful in smaller expressions, or when there is no Monad instance.
There are two infix operators for Functor.map.
g <$> x is short for Functor.map g x.
term ::= ...
| If `f : α → β` and `x : F α` then `f <$> x : F β`.
Conventions for notations in identifiers:
* The recommended spelling of `<$>` in identifiers is `map`.
x <&> g is short for Functor.map g x.
term ::= ... | term <&> term
g <*> x is short for Seq.seq g (fun () => x).
The function is inserted to delay evaluation because control might not reach the argument.
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.
Conventions for notations in identifiers:
* The recommended spelling of `<*>` in identifiers is `seq`.
e1 *> e2 is short for 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.
Conventions for notations in identifiers:
* The recommended spelling of `*>` in identifiers is `seqRight`.
e1 <* e2 is short for 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.
Conventions for notations in identifiers:
* The recommended spelling of `<*` in identifiers is `seqLeft`.
Many applicative functors also support failure and recovery via the Alternative type class.
This class also has an infix operator.
e <|> e' is short for OrElse.orElse e (fun () => e').
The function is inserted to delay evaluation because control might not reach the argument.
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`.structure User where
name : String
favoriteNat : Nat
def main : IO Unit := pure ()
Functor and Applicative Operators
A common functional programming idiom is to use a pure function in some context with effects by applying it via Functor.map and Seq.seq.
The function is applied to its sequence of arguments using <$>, and the arguments are separated by <*>.
In this example, the constructor User.mk is applied via this idiom in the body of 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)
When run with this input:
stdinA. Lean UserNone42it produces this output:
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 }
Monads are primarily used via Lean.Parser.Term.do : termdo-notation.
However, it can sometimes be convenient to describe monadic computations via operators.
act >>= f is syntax for 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`.
Conventions for notations in identifiers:
* The recommended spelling of `>>=` in identifiers is `bind`.
Similarly, the reversed operator f =<< act is syntax for Bind.bind act f.
term ::= ...
| Same as `Bind.bind` but with arguments swapped.
Conventions for notations in identifiers:
* The recommended spelling of `=<<` in identifiers is `bindLeft`.
The Kleisli composition operators Bind.kleisliRight and Bind.kleisliLeft also have infix operators.
term ::= ...
| Left-to-right composition of Kleisli arrows.
Conventions for notations in identifiers:
* The recommended spelling of `>=>` in identifiers is `kleisliRight`.term ::= ...
| Right-to-left composition of Kleisli arrows.
Conventions for notations in identifiers:
* The recommended spelling of `<=<` in identifiers is `kleisliLeft`.do-Notation
Monads are primarily used via Lean.Parser.Term.do : termdo-notation, which is an embedded language for programming in an imperative style.
It provides familiar syntax for sequencing effectful operations, early return, local mutable variables, loops, and exception handling.
All of these features are translated to the operations of the Monad type class, with a few of them requiring addition instances of classes such as ForIn that specify iteration over containers.
A Lean.Parser.Term.do : termdo term consists of the keyword Lean.Parser.Term.do : termdo followed by a sequence of Lean.Parser.Term.do : termdo items.
term ::= ... | do doSeqItem*
The items in a Lean.Parser.Term.do : termdo may be separated by semicolons; otherwise, each should be on its own line and they should have equal indentation.
One form of Lean.Parser.Term.do : termdo item is a term.
doSeqItem ::= ... | term
A term followed by a sequence of items is translated to a use bind; in particular, do e1; es is translated to e1 >>= fun () => do es.
| Desugaring |
|---|---|
do
e1
es | e1 >>= fun () => do es |
The result of the term's computation may also be named, allowing it to be used in subsequent steps.
This is done using Lean.Parser.Term.doLet : doElemlet.
There are two forms of monadic Lean.Parser.Term.doLet : doElemlet-binding in a Lean.Parser.Term.do : termdo block.
The first binds an identifier to the result, with an optional type annotation:
doSeqItem ::= ... | let ident(:term)? ← term
The second binds a pattern to the result.
The fallback clause, beginning with |, specifies the behavior when the pattern does not match the result.
doSeqItem ::= ... | let term ← term (| doSeq)?
This syntax is also translated to a use of bind.
do let x ← e1; es is translated to e1 >>= fun x => do es, and fallback clauses are translated to default pattern matches.
Lean.Parser.Term.doLet : doElemlet may also be used with the standard definition syntax := instead of ←.
This indicates a pure, rather than monadic, definition:
doSeqItem ::= ... | let(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).
do let x := e; es is translated to let x := e; do es.
| Desugaring |
|---|---|
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 |
Within a Lean.Parser.Term.do : termdo block, ← may be used as a prefix operator.
The expression to which it is applied is replaced with a fresh variable, which is bound using bind just before the current step.
This allows monadic effects to be used in positions that otherwise might expect a pure value, while still maintaining the distinction between describing an effectful computation and actually executing its effects.
Multiple occurrences of ← are processed from left to right, inside to outside.
Example | Desugaring |
|---|---|
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 |
In addition to convenient support for sequential computations with data dependencies, Lean.Parser.Term.do : termdo-notation also supports the local addition of a variety of effects, including early return, local mutable state, and loops with early termination.
These effects are implemented via transformations of the entire Lean.Parser.Term.do : termdo block in a manner akin to monad transformers, rather than via a local desugaring.
Early return terminates a computation immediately with a given value.
The value is returned from the closest containing Lean.Parser.Term.do : termdo block; however, this may not be the closest do keyword.
The rules for determining the extent of a Lean.Parser.Term.do : termdo block are described in their own section.
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 ()`.
Not all monads include early return.
Thus, when a Lean.Parser.Term.do : termdo block contains 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, the code needs to be rewritten to simulate the effect.
A program that uses early return to compute a value of type α in a monad m can be thought of as a program in the monad ExceptT α m α: early-returned values take the exception pathway, while ordinary returns do not.
Then, an outer handler can return the value from either code paths.
Internally, the Lean.Parser.Term.do : termdo elaborator performs a translation very much like this one.
On its own, 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 is short for 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().
Local mutable state is mutable state that cannot escape the Lean.Parser.Term.do : termdo block in which it is defined.
The Lean.Parser.Term.doLet : doElemlet mut binder introduces a locally-mutable binding.
Mutable bindings may be initialized either with pure computations or with monadic computations:
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
Similarly, they can be mutated either with pure values or the results of monad computations:
doElem ::= ... | ident(: term)? := term
doElem ::= ... | term(: term)? := term
doElem ::= ... | ident(: term)? ← term
doElem ::= ... | term ← term (| doSeq)?
These locally-mutable bindings are less powerful than a state monad because they are not mutable outside their lexical scope; this also makes them easier to reason about.
When Lean.Parser.Term.do : termdo blocks contain mutable bindings, the Lean.Parser.Term.do : termdo elaborator transforms the expression similarly to the way that StateT would, constructing a new monad and initializing it with the correct values.
There are Lean.Parser.Term.do : termdo items that correspond to most of Lean's term-level control structures.
When they occur as a step in a Lean.Parser.Term.do : termdo block, they are interpreted as Lean.Parser.Term.do : termdo items rather than terms.
Each branch of the control structures is a sequence of Lean.Parser.Term.do : termdo items, rather than a term, and some of them are more syntactically flexible than their corresponding terms.
In a Lean.Parser.Term.do : termdo block, Lean.Parser.Term.doIf : doElemif statements may omit their Lean.Parser.Term.doIf : doElemelse branch.
Omitting an Lean.Parser.Term.doIf : doElemelse branch is equivalent to using pure() as the contents of the branch.
doSeqItem ::= ... | if (ident :)? term then doSeqItem* (else doSeqItem*)?
Syntactically, the Lean.Parser.Term.doIf : doElemthen branch cannot be omitted.
For these cases, Lean.Parser.Term.doUnless : doElemunless only executes its body when the condition is false.
The Lean.Parser.Term.do : termdo in Lean.Parser.Term.doUnless : doElemunless is part of its syntax and does not induce a nested Lean.Parser.Term.do : termdo block.
doSeqItem ::= ... | unless term do doSeqItem*
When Lean.Parser.Term.doMatch : doElemmatch is used in a Lean.Parser.Term.do : termdo block, each branch is considered to be part of the same block.
Otherwise, it is equivalent to the 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 term.
doSeqItem ::= ... | match (((ident |`matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as `match h1 : e1, e2, h3 : e3 with ...`.hole ):)? term),* with (| term,* => doSeqItem*)*A *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).
Within a Lean.Parser.Term.do : termdo block, 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 loops allow iteration over a data structure.
The body of the loop is part of the containing Lean.Parser.Term.do : termdo block, so local effects such as early return and mutable variables may be used.
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.
A 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 loop requires at least one clause that specifies the iteration to be performed, which consists of an optional membership proof name followed by a colon (:), a pattern to bind, the keyword 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, and a collection term.
The pattern, which may just be an identifier, must match any element of the collection; patterns in this position cannot be used as implicit filters.
Further clauses may be provided by separating them with commas.
Each collection is iterated over at the same time, and iteration stops when any of the collections runs out of elements.
When iterating over multiple collections, iteration stops when any of the collections runs out of elements.
#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
When iterating over the valid indices for an array 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 `ToStream` typeclass.
for, naming the membership proof allows the tactic that searches for proofs that array indices are in bounds to succeed.
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
Omitting the hypothesis name causes the array lookup to fail, because no proof is available in the context that the iteration variable is within the specified range.
The body of a Lean.doElemWhile_Do_ : doElemwhile loop is repeated while the condition remains true.
It is possible to write infinite loops using them in functions that are not marked Lean.Parser.Command.declaration : commandpartial.
This is because the Lean.Parser.Command.declaration : commandpartial modifier only applies to non-termination or infinite regress induced by the function being defined, and not by those that it calls.
The translation of Lean.doElemWhile_Do_ : doElemwhile loops relies on a separate helper.
doSeqItem ::= ... | while term do doSeqItem*
doSeqItem ::= ... | while ident : term do doSeqItem*
The body of a Lean.doElemRepeat_ : doElemrepeat loop is repeated until a Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break statement is executed.
Just like Lean.doElemWhile_Do_ : doElemwhile loops, these loops can be used in functions that are not marked Lean.Parser.Command.declaration : commandpartial.
doSeqItem ::= ... | repeat doSeqItem*
The Lean.Parser.Term.doContinue : doElem`continue` skips to the next iteration of the surrounding `for` loop. continue statement skips the rest of the body of the closest enclosing Lean.doElemRepeat_ : doElemrepeat, Lean.doElemWhile_Do_ : doElemwhile, or 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 loop, moving on to the next iteration.
The Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break statement terminates the closest enclosing Lean.doElemRepeat_ : doElemrepeat, Lean.doElemWhile_Do_ : doElemwhile, or 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 loop, stopping iteration.
doSeqItem ::= ...
| `continue` skips to the next iteration of the surrounding `for` loop. doSeqItem ::= ...
| `break` exits the surrounding `for` loop.
In addition to Lean.Parser.Term.doBreak : doElem`break` exits the surrounding `for` loop. break, loops can always be terminated by effects in the current monad.
Throwing an exception from a loop terminates the loop.
do Blocks
Many features of Lean.Parser.Term.do : termdo-notation have an effect on the current Lean.Parser.Term.do : termdo block.
In particular, early return aborts the current block, causing it to evaluate to the returned value, and mutable bindings can only be mutated in the block in which they are defined.
Understanding these features requires a precise definition of what it means to be in the “same” block.
Empirically, this can be checked using the Lean language server.
When the cursor is on a 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 statement, the corresponding Lean.Parser.Term.do : termdo keyword is highlighted.
Attempting to mutate a mutable binding outside of the same Lean.Parser.Term.do : termdo block results in an error message.
Lean.Parser.Term.do : termdoThe rules are as follows:
Each item immediately nested under the Lean.Parser.Term.do : termdo keyword that begins a block belongs to that block.
Each item immediately nested under the Lean.Parser.Term.do : termdo keyword that is an item in a containing Lean.Parser.Term.do : termdo block belongs to the outer block.
Items in the branches of an Lean.Parser.Term.doIf : doElemif, Lean.Parser.Term.doMatch : doElemmatch, or Lean.Parser.Term.doUnless : doElemunless item belong to the same Lean.Parser.Term.do : termdo block as the control structure that contains them. The Lean.Parser.Term.doUnless : doElemdo keyword that is part of the syntax of Lean.Parser.Term.doUnless : doElemunless does not introduce a new Lean.Parser.Term.do : termdo block.
Items in the body of Lean.doElemRepeat_ : doElemrepeat, Lean.doElemWhile_Do_ : doElemwhile, and 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 belong to the same Lean.Parser.Term.do : termdo block as the loop that contains them. The 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 keyword that is part of the syntax of Lean.doElemWhile_Do_ : doElemwhile and 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 does not introduce a new Lean.Parser.Term.do : termdo block.
do and Branches
The following example outputs 6 rather than 7:
def test : StateM Nat Unit := do
set 5
if true then
set 6
do return
set 7
return
#eval test.run 0
((), 6)
This is because the 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 statement under the Lean.Parser.Term.doIf : doElemif belongs to the same Lean.Parser.Term.do : termdo as its immediate parent, which itself belongs to the same Lean.Parser.Term.do : termdo as the Lean.Parser.Term.doIf : doElemif.
If Lean.Parser.Term.do : termdo blocks that occurred as items in other Lean.Parser.Term.do : termdo blocks instead created new blocks, then the example would output 7.
To be used 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 `ToStream` typeclass.
for loops without membership proofs, collections must implement the ForIn type class.
Implementing ForIn' additionally allows the use of 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 loops with membership proofs.
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.
ForIn.mk.{u, v, u₁, u₂}
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.)
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.
ForIn'.mk.{u, v, u₁, u₂}
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.
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 and a is the new state.
.yield is produced by continue and reaching the bottom of the loop body.
.done (a : α), meaning that we should early-exit the loop with state a.
.done is produced by calls to break or return in the loop,
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.
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 only m and γ.
ForM.mk.{u, v, w₁, w₂}
forM : [inst : Monad m] → γ → (α → m PUnit) → m PUnit