@[inline]

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

def Lean.Parser.Term.leftArrow : Parser

def Lean.Parser.Term.liftMethod : Parser

def Lean.Parser.Term.doSeqItem : Parser

def Lean.Parser.Term.doSeqIndent : Parser

def Lean.Parser.Term.doSeqBracketed : Parser

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.

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.

def Lean.Parser.Term.notFollowedByRedefinedTermToken : Parser

def Lean.Parser.Term.doLet : Parser

def Lean.Parser.Term.doLetElse : Parser

def Lean.Parser.Term.doLetExpr : Parser

def Lean.Parser.Term.doLetMetaExpr : Parser

def Lean.Parser.Term.doLetRec : Parser

def Lean.Parser.Term.doIdDecl : Parser

def Lean.Parser.Term.doPatDecl : Parser

def Lean.Parser.Term.doLetArrow : Parser

def Lean.Parser.Term.letIdDeclNoBinders : Parser

def Lean.Parser.Term.doReassign : Parser

def Lean.Parser.Term.doReassignArrow : Parser

def Lean.Parser.Term.doHave : Parser

def Lean.Parser.Term.elseIf : Parser

def Lean.Parser.Term.doIfLetPure : Parser

def Lean.Parser.Term.doIfLetBind : Parser

def Lean.Parser.Term.doIfLet : Parser

def Lean.Parser.Term.doIfProp : Parser

def Lean.Parser.Term.doIfCond : Parser

def Lean.Parser.Term.doIf : Parser

def Lean.Parser.Term.doUnless : Parser

def Lean.Parser.Term.doForDecl : Parser

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

def Lean.Parser.Term.doMatchAlts : Parser

def Lean.Parser.Term.doMatch : Parser

def Lean.Parser.Term.doMatchExprAlts : Parser

def Lean.Parser.Term.optMetaFalse : Parser

def Lean.Parser.Term.doMatchExpr : Parser

def Lean.Parser.Term.doCatch : Parser

def Lean.Parser.Term.doCatchMatch : Parser

def Lean.Parser.Term.doFinally : Parser

def Lean.Parser.Term.doTry : Parser

def Lean.Parser.Term.doBreak : Parser

break exits the surrounding for loop.

def Lean.Parser.Term.doContinue : Parser

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

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

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.

def Lean.Parser.Term.doAssert : Parser

assert! cond panics if cond evaluates to false.

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

def Lean.Parser.Term.doExpr : Parser

def Lean.Parser.Term.doNested : Parser

def Lean.Parser.Term.do : Parser

def Lean.Parser.Term.termUnless : Parser

unless e do s is a nicer way to write if !e do s.

def Lean.Parser.Term.termFor : Parser

def Lean.Parser.Term.termTry : Parser

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.