@[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.liftMethod : 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 : TSyntax `Lean.Parser.Term.doSeq) : Array (TSyntax `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.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 of 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.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.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.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.