@[inline]

def Lean.Parser.doElemParser (rbp : Nat := 0) : Parser

Equations

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

def Lean.Parser.Term.leftArrow : Parser

Equations

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

def Lean.Parser.Term.nestedAction : Parser

Equations

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

def Lean.Parser.Term.doSeqItem : Parser

Equations

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

def Lean.Parser.Term.doSeqIndent : Parser

Equations

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

def Lean.Parser.Term.doSeqBracketed : Parser

Equations

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

def Lean.Parser.Term.doSeq : Parser

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)

def Lean.Parser.Term.termBeforeDo : Parser

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

def Lean.Parser.Term.getDoElems (doSeq : DoSeq) : Array DoElem

Equations

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

def Lean.Parser.Term.notFollowedByRedefinedTermToken : Parser

Equations

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

def Lean.Parser.Term.InternalSyntax.doSkip : ParserDescr

Internal syntax used in the if and unless elaborators. Behaves like pure PUnit.unit but uses () if possible and gives better error messages.

Equations

• Lean.Parser.Term.InternalSyntax.doSkip = Lean.ParserDescr.node `Lean.Parser.Term.InternalSyntax.doSkip 1024 (Lean.ParserDescr.symbol "skip")

def Lean.Parser.Term.doLet : Parser

Equations

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

def Lean.Parser.Term.doLetElse : Parser

Equations

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

def Lean.Parser.Term.doLetExpr : Parser

Equations

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

def Lean.Parser.Term.doLetMetaExpr : Parser

Equations

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

def Lean.Parser.Term.doLetRec : Parser

Equations

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

def Lean.Parser.Term.doIdDecl : Parser

Equations

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

def Lean.Parser.Term.doPatDecl : Parser

Equations

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

def Lean.Parser.Term.doLetArrow : Parser

Equations

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

def Lean.Parser.Term.letIdDeclNoBinders : Parser

Equations

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

def Lean.Parser.Term.doReassign : Parser

Equations

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

def Lean.Parser.Term.doReassignArrow : Parser

Equations

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

def Lean.Parser.Term.doHave : Parser

Equations

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

def Lean.Parser.Term.elseIf : Parser

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 ")))

def Lean.Parser.Term.doIfLetPure : Parser

Equations

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

def Lean.Parser.Term.doIfLetBind : Parser

Equations

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

def Lean.Parser.Term.doIfLet : Parser

Equations

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

def Lean.Parser.Term.doIfProp : Parser

Equations

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

def Lean.Parser.Term.doIfCond : Parser

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)

def Lean.Parser.Term.doIf : Parser

Equations

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

def Lean.Parser.Term.doUnless : Parser

Equations

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

def Lean.Parser.Term.doForDecl : Parser

Equations

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

def Lean.Parser.Term.doFor : Parser

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 over the given collections in parallel, until at least one of them is exhausted. The types of e2 etc. must implement the Std.ToStream typeclass.

Equations

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

def Lean.Parser.Term.dependentParam : Parser

Equations

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

def Lean.Parser.Term.doMatchAlts : Parser

Equations

• Lean.Parser.Term.doMatchAlts = Lean.Parser.ppDedent (Lean.Parser.Term.matchAlts Lean.Parser.Term.doSeq)

def Lean.Parser.Term.doMatch : Parser

Equations

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

def Lean.Parser.Term.doMatchExprAlts : Parser

Equations

• Lean.Parser.Term.doMatchExprAlts = Lean.Parser.ppDedent (Lean.Parser.Term.matchExprAlts Lean.Parser.Term.doSeq)

def Lean.Parser.Term.optMetaFalse : Parser

Equations

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

def Lean.Parser.Term.doMatchExpr : Parser

Equations

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

def Lean.Parser.Term.doCatch : Parser

Equations

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

def Lean.Parser.Term.doCatchMatch : Parser

Equations

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

def Lean.Parser.Term.doFinally : Parser

Equations

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

def Lean.Parser.Term.doTry : Parser

Equations

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

def Lean.Parser.Term.doForward : Parser

do← s (or ASCII do<- s) hands s to the enclosing wrapper as a body whose control-flow effects (return, break, continue, mut-variable reassignment) target the surrounding do block, not the body's local monad.

The syntax is reminiscent of a nested action (← s), but unlike a nested action, s is not run eagerly in the do block context before the wrapping function is called. The wrapping function decides when to run s, and code is inserted to forward s's effects to the outer do block.

Only valid as the last argument of a function application that itself appears as a statement of an outer do block, optionally wrapped in fun binders. Examples:

• f a₁ … aₙ (do← s)
• f a₁ … aₙ (fun b₁ … bₖ => do← s)

Equations

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

def Lean.Parser.Term.doBreak : Parser

break exits the surrounding for loop.

Equations

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

def Lean.Parser.Term.doContinue : Parser

continue skips to the next iteration of the surrounding for loop.

Equations

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

def Lean.Parser.Term.doReturn : Parser

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.

def Lean.Parser.Term.doDbgTrace : Parser

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.

def Lean.Parser.Term.doIdbg : Parser

experimental

idbg e enables live inspection of program state from the editor. When placed in a do block, it captures all local variables in scope and the expression e, then:

• In the language server: starts a TCP server on localhost waiting for the running program to connect; the editor will mark this part of the program as "in progress" during this wait but that will not block lake build of the project.
• In the compiled program: on first execution of the idbg call site, connects to the server, receives the expression, compiles and evaluates it using the program's actual runtime values, and sends the repr result back.

The result is displayed as an info diagnostic on the idbg keyword. The expression e can be edited while the program is running - each edit triggers re-elaboration of e, a new TCP exchange, and an updated result. This makes idbg a live REPL for inspecting and experimenting with program state at a specific point in execution. Only when idbg is inserted, moved, or removed does the program need to be recompiled and restarted.

Known Limitations

• The program will poll the server for up to 10 minutes and needs to be killed manually otherwise.
• Use of multiple idbg at once untested, likely too much overhead from overlapping imports without further changes.
• LEAN_PATH must be properly set up so the compiled program can import its origin module.
• Untested on Windows and macOS.

Equations

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

def Lean.Parser.Term.doAssert : Parser

assert! cond panics if cond evaluates to false.

Equations

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

def Lean.Parser.Term.doDebugAssert : Parser

debug_assert! cond panics if cond evaluates to false and the executing code has been built with debug assertions enabled (see the debugAssertions option).

Equations

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

def Lean.Parser.Term.doRepeat : Parser

Equations

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

def Lean.Parser.Term.doWhile : Parser

Equations

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

def Lean.Parser.Term.doRepeatUntil : Parser

Equations

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

def Lean.Parser.Term.doExpr : Parser

Equations

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

def Lean.Parser.Term.doNested : Parser

Equations

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

def Lean.Parser.Term.do : Parser

Equations

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

def Lean.Parser.Term.termUnless : Parser

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.

def Lean.Parser.Term.termFor : Parser

Equations

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

def Lean.Parser.Term.termTry : Parser

Equations

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

def Lean.Parser.Term.termReturn : Parser

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.