7.3. Syntax

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.

7.3.1. Infix Operators

Infix operators are primarily useful in smaller expressions, or when there is no Monad instance.

7.3.1.1. Functors

There are two infix operators for Functor.map.

syntaxFunctor Operators

g <$> x is short for Functor.map g x.

term ::= ...
    | If `f : α → β` and `x : F α` then `f <$> x : F β`. term <$> term

x <&> g is short for Functor.map g x.

term ::= ...
    | term <&> term

7.3.1.2. Applicative Functors

syntaxApplicative Operators

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. term <*> term

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. term *> term

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. term <* term

Many applicative functors also support failure and recovery via the Alternative type class. This class also has an infix operator.

syntaxAlternative Operators

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. term <|> term

structure User where
  name : String
  favoriteNat : Nat
def main : IO Unit := pure ()

Infix 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 UserNone42

it 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 }

7.3.1.3. Monads

Monads are primarily used via Lean.Parser.Term.do : termdo-notation. However, it can sometimes be convenient to describe monadic computations via operators.

syntaxMonad 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`. term >>= term

Similarly, the reversed operator f =<< act is syntax for Bind.bind act f.

term ::= ...
    | Same as `Bind.bind` but with arguments swapped. term =<< term

The Kleisli composition operators Bind.kleisliRight and Bind.kleisliLeft also have infix operators.

term ::= ...
    | Left-to-right composition of Kleisli arrows. term >=> term

term ::= ...
    | Right-to-left composition of Kleisli arrows. term <=< term

7.3.2. `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.

syntax

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.

7.3.2.1. Sequential Computations

One form of Lean.Parser.Term.do : termdo item is a term.

syntax

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.

`Lean.Parser.Term.do : termdo` Item	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.

syntax

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:

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. v := term

do let x := e; es is translated to let x := e; do es.

`Lean.Parser.Term.do : termdo` Item	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 `Lean.Parser.Term.do : termdo` Item	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`

Example Nested Action Desugarings

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.

7.3.2.2. Early Return

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.

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 ()`.
return term

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

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().

7.3.2.3. Local Mutable State

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.

syntax

Mutable bindings may be initialized either with pure computations or with monadic computations:

doSeqItem ::= ...
    | let mut `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. (ident  | 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).
hole ):= term

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.

7.3.2.4. Control Structures🔗

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.

syntax

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.

syntax

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.

syntax

doSeqItem ::= ...
    | match (`matchDiscr` matches a "match discriminant", either `h : tm` or `tm`, used in `match` as
`match h1 : e1, e2, h3 : e3 with ...`. (ident :)? term),* with
        (| term,* => doSeqItem*)*

7.3.2.5. Iteration

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.

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.
for ((ident :)? term in term),* do
        doSeqItem*

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.

Iteration Over Multiple Collections

When iterating over multiple collections, iteration stops when any of the collections runs out of elements.

#[(0, 'a'), (1, 'b')]#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')]

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 `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.

syntax

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.

syntax

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.

syntax

doSeqItem ::= ...
    | `continue` skips to the next iteration of the surrounding `for` loop. continue

doSeqItem ::= ...
    | `break` exits the surrounding `for` loop. break

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.

Terminating Loops in the Option Monad

The failure method from the Alternative class can be used to terminate an otherwise-infinite loop in the Option monad.

none#eval show Option Nat from do
  let mut i := 0
  repeat
    if i > 1000 then failure
    else i := 2 * (i + 1)
  return i

none

7.3.2.6. Identifying `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.

Highlighting `Lean.Parser.Term.do : termdo`

The 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.

Nested 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

((), 6)#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.

7.3.2.7. Type Classes for Iteration

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.

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 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,

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 only m and γ.

Instance Constructor

ForM.mk.{u, v, w₁, w₂}

Methods

forM : [inst : Monad m] → γ → (α → m PUnit) → m PUnit

def

ForM.forIn.{u_1, u_2, u_3, u_4}
    {m : Type u_1 → Type u_2} {β : Type u_1}
    {ρ : Type u_3} {α : Type u_4} [Monad m]
    [ForM (StateT β (ExceptT β m)) ρ α] (x : ρ)
    (b : β) (f : α → β → m (ForInStep β)) : m β

Adapter to create a ForIn instance from a ForM instance

7.3. Syntax

7.3.1. Infix Operators

7.3.1.1. Functors

7.3.1.2. Applicative Functors

7.3.1.3. Monads

7.3.2. do-Notation🔗

7.3.2.1. Sequential Computations

7.3.2.2. Early Return

7.3.2.3. Local Mutable State

7.3.2.4. Control Structures🔗

7.3.2.5. Iteration

7.3.2.6. Identifying do Blocks🔗

7.3.2.7. Type Classes for Iteration

Instance Constructor

Methods

Instance Constructor

Methods

Constructors

Instance Constructor

Methods

7.3.2. `do`-Notation🔗

7.3.2.6. Identifying `do` Blocks🔗