## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

`break`

exits the surrounding `for`

loop.

## Equations

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

`continue`

skips to the next iteration of the surrounding `for`

loop.

## Equations

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

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

## Equations

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

`unless e do s`

is a nicer way to write `if !e do s`

.

## Equations

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

## Equations

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

## Equations

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

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