## Equations

- Lean.Parser.doElemParser rbp = Lean.Parser.categoryParser `doElem rbp

## Instances For

## Equations

- Lean.Parser.Term.leftArrow = Lean.Parser.unicodeSymbol "← " "<- "

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

A `doSeq`

is a sequence of `doElem`

, the main argument after the `do`

keyword and other
do elements that take blocks. It can either have the form `"{" (doElem ";"?)* "}"`

or
`many1Indent (doElem ";"?)`

, where `many1Indent`

ensures that all the items are at
the same or higher indentation level as the first line.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`termBeforeDo`

is defined as `withForbidden("do", term)`

, which will parse a term but
disallows `do`

outside of a bracketing construct. This is used for parsers like `for _ in t do ...`

or `unless t do ...`

, where we do not want `t do ...`

to be parsed as an application of `t`

to a
`do`

block, which would otherwise be allowed.

## Equations

- Lean.Parser.Term.termBeforeDo = Lean.Parser.withForbidden "do" Lean.Parser.termParser

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`break`

exits the surrounding `for`

loop.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`continue`

skips to the next iteration of the surrounding `for`

loop.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`dbg_trace e`

prints `e`

(which can be an interpolated string literal) to stderr.
It should only be used for debugging.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`return`

used outside of `do`

blocks creates an implicit block around it
and thus is equivalent to `pure e`

, but helps with avoiding parentheses.

## Equations

- One or more equations did not get rendered due to their size.