@[inline]

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

Equations

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

def Lean.Parser.Term.leftArrow : Lean.Parser.Parser

def Lean.Parser.Term.liftMethod : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doSeqItem : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doSeqIndent : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doSeqBracketed : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doSeq : Lean.Parser.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 : Lean.Parser.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.notFollowedByRedefinedTermToken : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doLet : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doLetElse : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doLetExpr : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doLetMetaExpr : Lean.Parser.Parser

def Lean.Parser.Term.doLetRec : Lean.Parser.Parser

def Lean.Parser.Term.doIdDecl : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doPatDecl : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doLetArrow : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.letIdDeclNoBinders : Lean.Parser.Parser

def Lean.Parser.Term.doReassign : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doReassignArrow : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doHave : Lean.Parser.Parser

def Lean.Parser.Term.elseIf : Lean.Parser.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 : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doIfLetBind : Lean.Parser.Parser

def Lean.Parser.Term.doIfLet : Lean.Parser.Parser

def Lean.Parser.Term.doIfProp : Lean.Parser.Parser

def Lean.Parser.Term.doIfCond : Lean.Parser.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 : Lean.Parser.Parser

def Lean.Parser.Term.doUnless : Lean.Parser.Parser

def Lean.Parser.Term.doForDecl : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doFor : Lean.Parser.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.

Equations

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

def Lean.Parser.Term.doMatchAlts : Lean.Parser.Parser

def Lean.Parser.Term.doMatch : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doMatchExprAlts : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.optMetaFalse : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doMatchExpr : Lean.Parser.Parser

def Lean.Parser.Term.doCatch : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doCatchMatch : Lean.Parser.Parser

def Lean.Parser.Term.doFinally : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.doTry : Lean.Parser.Parser

def Lean.Parser.Term.doBreak : Lean.Parser.Parser

break exits the surrounding for loop.

def Lean.Parser.Term.doContinue : Lean.Parser.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 : Lean.Parser.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 : Lean.Parser.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 : Lean.Parser.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.doExpr : Lean.Parser.Parser

def Lean.Parser.Term.doNested : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.do : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.termUnless : Lean.Parser.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 : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.termTry : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.termReturn : Lean.Parser.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.