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.
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
- Lean.Parser.Term.doSeq = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doSeq" `Lean.Parser.Term.doSeq true true) (Lean.Parser.Term.doSeqBracketed <|> Lean.Parser.Term.doSeqIndent)
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
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
- Lean.Parser.Term.elseIf = Lean.Parser.atomic (Lean.Parser.group (Lean.Parser.withPosition (Lean.Parser.symbol "else " >> Lean.Parser.checkLineEq >> Lean.Parser.symbol " if ")))
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.doIfCond = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doIfCond" `Lean.Parser.Term.doIfCond false true) (Lean.Parser.Term.doIfLet <|> Lean.Parser.Term.doIfProp)
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.
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.
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.
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.
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.