Lean.Parser.Do

source

@[inline]

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

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.leftArrow :

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.liftMethod :

Lean.Parser.Parser

Equations

Lean.Parser.Term.liftMethod = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "liftMethod" (some `Lean.Parser.Term.liftMethod)) (Lean.Parser.leadingNode `Lean.Parser.Term.liftMethod Lean.Parser.minPrec (HAndThen.hAndThen Lean.Parser.Term.leftArrow fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.doSeqItem :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doSeqItem = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doSeqItem" (some `Lean.Parser.Term.doSeqItem)) (Lean.Parser.leadingNode `Lean.Parser.Term.doSeqItem 1024 (HAndThen.hAndThen Lean.Parser.ppLine fun x => HAndThen.hAndThen Lean.Parser.doElemParser fun x => Lean.Parser.optional (Lean.Parser.symbol "; ")))

source

def Lean.Parser.Term.doSeqIndent :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doSeqIndent = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doSeqIndent" (some `Lean.Parser.Term.doSeqIndent)) (Lean.Parser.leadingNode `Lean.Parser.Term.doSeqIndent 1024 (Lean.Parser.many1Indent Lean.Parser.Term.doSeqItem))

source

def Lean.Parser.Term.doSeqBracketed :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doSeqBracketed = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doSeqBracketed" (some `Lean.Parser.Term.doSeqBracketed)) (Lean.Parser.leadingNode `Lean.Parser.Term.doSeqBracketed 1024 (HAndThen.hAndThen (Lean.Parser.symbol "{") fun x => HAndThen.hAndThen (Lean.Parser.withoutPosition (Lean.Parser.many1 Lean.Parser.Term.doSeqItem)) fun x => HAndThen.hAndThen Lean.Parser.ppLine fun x => Lean.Parser.symbol "}"))

source

def Lean.Parser.Term.doSeq :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doSeq = HOrElse.hOrElse Lean.Parser.Term.doSeqBracketed fun x => Lean.Parser.Term.doSeqIndent

source

def Lean.Parser.Term.termBeforeDo :

Lean.Parser.Parser

Equations

Lean.Parser.Term.termBeforeDo = Lean.Parser.withForbidden "do" Lean.Parser.termParser

source

def Lean.Parser.Term.notFollowedByRedefinedTermToken :

Lean.Parser.Parser

Equations

Lean.Parser.Term.notFollowedByRedefinedTermToken = Lean.Parser.notFollowedBy (HOrElse.hOrElse (Lean.Parser.symbol "set_option") fun x => HOrElse.hOrElse (Lean.Parser.symbol "open") fun x => HOrElse.hOrElse (Lean.Parser.symbol "if") fun x => HOrElse.hOrElse (Lean.Parser.symbol "match") fun x => HOrElse.hOrElse (Lean.Parser.symbol "let") fun x => HOrElse.hOrElse (Lean.Parser.symbol "have") fun x => HOrElse.hOrElse (Lean.Parser.symbol "do") fun x => HOrElse.hOrElse (Lean.Parser.symbol "dbg_trace") fun x => HOrElse.hOrElse (Lean.Parser.symbol "assert!") fun x => HOrElse.hOrElse (Lean.Parser.symbol "for") fun x => HOrElse.hOrElse (Lean.Parser.symbol "unless") fun x => HOrElse.hOrElse (Lean.Parser.symbol "return") fun x => Lean.Parser.symbol "try") "token at 'do' element"

source

def Lean.Parser.Term.doLet :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doLet = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doLet" (some `Lean.Parser.Term.doLet)) (Lean.Parser.leadingNode `Lean.Parser.Term.doLet 1024 (HAndThen.hAndThen (Lean.Parser.symbol "let ") fun x => HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.symbol "mut ")) fun x => Lean.Parser.Term.letDecl))

source

def Lean.Parser.Term.doLetElse :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doLetElse = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doLetElse" (some `Lean.Parser.Term.doLetElse)) (Lean.Parser.leadingNode `Lean.Parser.Term.doLetElse 1024 (HAndThen.hAndThen (Lean.Parser.symbol "let ") fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => HAndThen.hAndThen Lean.Parser.checkColGt fun x => HAndThen.hAndThen (Lean.Parser.symbol " | ") fun x => Lean.Parser.doElemParser))

source

def Lean.Parser.Term.doLetRec :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doLetRec = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doLetRec" (some `Lean.Parser.Term.doLetRec)) (Lean.Parser.leadingNode `Lean.Parser.Term.doLetRec 1024 (HAndThen.hAndThen (Lean.Parser.group (HAndThen.hAndThen (Lean.Parser.symbol "let ") fun x => Lean.Parser.nonReservedSymbol "rec ")) fun x => Lean.Parser.Term.letRecDecls))

source

def Lean.Parser.Term.doIdDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doIdDecl = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doIdDecl" (some `Lean.Parser.Term.doIdDecl)) (Lean.Parser.leadingNode `Lean.Parser.Term.doIdDecl 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen Lean.Parser.Term.optType fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Term.leftArrow)) fun x => Lean.Parser.doElemParser))

source

def Lean.Parser.Term.doPatDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doPatDecl = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doPatDecl" (some `Lean.Parser.Term.doPatDecl)) (Lean.Parser.leadingNode `Lean.Parser.Term.doPatDecl 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.termParser fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Term.leftArrow)) fun x => HAndThen.hAndThen Lean.Parser.doElemParser fun x => Lean.Parser.optional (HAndThen.hAndThen Lean.Parser.checkColGt fun x => HAndThen.hAndThen (Lean.Parser.symbol " | ") fun x => Lean.Parser.doElemParser)))

source

def Lean.Parser.Term.doLetArrow :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doLetArrow = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doLetArrow" (some `Lean.Parser.Term.doLetArrow)) (Lean.Parser.leadingNode `Lean.Parser.Term.doLetArrow 1024 (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "let ") fun x => HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.symbol "mut ")) fun x => HOrElse.hOrElse Lean.Parser.Term.doIdDecl fun x => Lean.Parser.Term.doPatDecl)))

source

def Lean.Parser.Term.letIdDeclNoBinders :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letIdDeclNoBinders = Lean.Parser.node `Lean.Parser.Term.letIdDecl (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen Lean.Parser.pushNone fun x => HAndThen.hAndThen Lean.Parser.Term.optType fun x => Lean.Parser.symbol " := ")) fun x => Lean.Parser.termParser)

source

def Lean.Parser.Term.doReassign :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doReassign = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doReassign" (some `Lean.Parser.Term.doReassign)) (Lean.Parser.leadingNode `Lean.Parser.Term.doReassign 1024 (HAndThen.hAndThen Lean.Parser.Term.notFollowedByRedefinedTermToken fun x => HOrElse.hOrElse Lean.Parser.Term.letIdDeclNoBinders fun x => Lean.Parser.Term.letPatDecl))

source

def Lean.Parser.Term.doReassignArrow :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doReassignArrow = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doReassignArrow" (some `Lean.Parser.Term.doReassignArrow)) (Lean.Parser.leadingNode `Lean.Parser.Term.doReassignArrow 1024 (HAndThen.hAndThen Lean.Parser.Term.notFollowedByRedefinedTermToken fun x => Lean.Parser.withPosition (HOrElse.hOrElse Lean.Parser.Term.doIdDecl fun x => Lean.Parser.Term.doPatDecl)))

source

def Lean.Parser.Term.doHave :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doHave = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doHave" (some `Lean.Parser.Term.doHave)) (Lean.Parser.leadingNode `Lean.Parser.Term.doHave 1024 (HAndThen.hAndThen (Lean.Parser.symbol "have ") fun x => Lean.Parser.Term.haveDecl))

source

def Lean.Parser.Term.elseIf :

Lean.Parser.Parser

Equations

Lean.Parser.Term.elseIf = Lean.Parser.atomic (Lean.Parser.group (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol " else ") fun x => HAndThen.hAndThen Lean.Parser.checkLineEq fun x => Lean.Parser.symbol " if ")))

source

def Lean.Parser.Term.doIfLetPure :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doIfLetPure = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doIfLetPure" (some `Lean.Parser.Term.doIfLetPure)) (Lean.Parser.leadingNode `Lean.Parser.Term.doIfLetPure 1024 (HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.doIfLetBind :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doIfLetBind = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doIfLetBind" (some `Lean.Parser.Term.doIfLetBind)) (Lean.Parser.leadingNode `Lean.Parser.Term.doIfLetBind 1024 (HAndThen.hAndThen (Lean.Parser.symbol " ← ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.doIfLet :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doIfLet = Lean.Parser.nodeWithAntiquot "doIfLet" `Lean.Parser.Term.doIfLet (HAndThen.hAndThen (Lean.Parser.symbol "let ") fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => HOrElse.hOrElse Lean.Parser.Term.doIfLetPure fun x => Lean.Parser.Term.doIfLetBind)

source

def Lean.Parser.Term.doIfProp :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doIfProp = Lean.Parser.nodeWithAntiquot "doIfProp" `Lean.Parser.Term.doIfProp (HAndThen.hAndThen Lean.Parser.Term.optIdent fun x => Lean.Parser.termParser)

source

def Lean.Parser.Term.doIf :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doIf = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doIf" (some `Lean.Parser.Term.doIf)) (Lean.Parser.leadingNode `Lean.Parser.Term.doIf 1024 (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "if ") fun x => HAndThen.hAndThen Lean.Parser.Term.doIfCond fun x => HAndThen.hAndThen (Lean.Parser.symbol " then ") fun x => HAndThen.hAndThen Lean.Parser.Term.doSeq fun x => HAndThen.hAndThen (Lean.Parser.many (HAndThen.hAndThen (Lean.Parser.checkColGe "'else if' in 'do' must be indented") fun x => Lean.Parser.group (HAndThen.hAndThen Lean.Parser.Term.elseIf fun x => HAndThen.hAndThen Lean.Parser.Term.doIfCond fun x => HAndThen.hAndThen (Lean.Parser.symbol " then ") fun x => Lean.Parser.Term.doSeq))) fun x => Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.checkColGe "'else' in 'do' must be indented") fun x => HAndThen.hAndThen (Lean.Parser.symbol " else ") fun x => Lean.Parser.Term.doSeq))))

source

def Lean.Parser.Term.doIfCond :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doIfCond = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doIfCond" none false) (HOrElse.hOrElse Lean.Parser.Term.doIfLet fun x => Lean.Parser.Term.doIfProp)

source

def Lean.Parser.Term.doUnless :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doUnless = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doUnless" (some `Lean.Parser.Term.doUnless)) (Lean.Parser.leadingNode `Lean.Parser.Term.doUnless 1024 (HAndThen.hAndThen (Lean.Parser.symbol "unless ") fun x => HAndThen.hAndThen (Lean.Parser.withForbidden "do" Lean.Parser.termParser) fun x => HAndThen.hAndThen (Lean.Parser.symbol "do ") fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Term.doForDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doForDecl = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doForDecl" (some `Lean.Parser.Term.doForDecl)) (Lean.Parser.leadingNode `Lean.Parser.Term.doForDecl 1024 (HAndThen.hAndThen Lean.Parser.termParser fun x => HAndThen.hAndThen (Lean.Parser.symbol " in ") fun x => Lean.Parser.withForbidden "do" Lean.Parser.termParser))

source

def Lean.Parser.Term.doFor :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doFor = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doFor" (some `Lean.Parser.Term.doFor)) (Lean.Parser.leadingNode `Lean.Parser.Term.doFor 1024 (HAndThen.hAndThen (Lean.Parser.symbol "for ") fun x => HAndThen.hAndThen (Lean.Parser.sepBy1 Lean.Parser.Term.doForDecl ", " (Lean.Parser.symbol ", ")) fun x => HAndThen.hAndThen (Lean.Parser.symbol "do ") fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Term.doMatch :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doMatch = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doMatch" (some `Lean.Parser.Term.doMatch)) (Lean.Parser.leadingNode `Lean.Parser.Term.doMatch Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "match ") fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Term.generalizingParam) fun x => HAndThen.hAndThen (Lean.Parser.sepBy1 Lean.Parser.Term.matchDiscr ", " (Lean.Parser.symbol ", ")) fun x => HAndThen.hAndThen Lean.Parser.Term.optType fun x => HAndThen.hAndThen (Lean.Parser.symbol " with ") fun x => Lean.Parser.Term.doMatchAlts))

source

def Lean.Parser.Term.doMatchAlts :

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doCatch :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doCatch = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doCatch" (some `Lean.Parser.Term.doCatch)) (Lean.Parser.leadingNode `Lean.Parser.Term.doCatch 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol "catch ") fun x => Lean.Parser.Term.binderIdent)) fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.termParser)) fun x => HAndThen.hAndThen Lean.Parser.darrow fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Term.doCatchMatch :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doCatchMatch = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doCatchMatch" (some `Lean.Parser.Term.doCatchMatch)) (Lean.Parser.leadingNode `Lean.Parser.Term.doCatchMatch 1024 (HAndThen.hAndThen (Lean.Parser.symbol "catch ") fun x => Lean.Parser.Term.doMatchAlts))

source

def Lean.Parser.Term.doTry :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doTry = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doTry" (some `Lean.Parser.Term.doTry)) (Lean.Parser.leadingNode `Lean.Parser.Term.doTry 1024 (HAndThen.hAndThen (Lean.Parser.symbol "try ") fun x => HAndThen.hAndThen Lean.Parser.Term.doSeq fun x => HAndThen.hAndThen (Lean.Parser.many (HOrElse.hOrElse Lean.Parser.Term.doCatch fun x => Lean.Parser.Term.doCatchMatch)) fun x => Lean.Parser.optional Lean.Parser.Term.doFinally))

source

def Lean.Parser.Term.doFinally :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doFinally = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doFinally" (some `Lean.Parser.Term.doFinally)) (Lean.Parser.leadingNode `Lean.Parser.Term.doFinally 1024 (HAndThen.hAndThen (Lean.Parser.symbol "finally ") fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Term.doBreak :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doBreak = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doBreak" (some `Lean.Parser.Term.doBreak)) (Lean.Parser.leadingNode `Lean.Parser.Term.doBreak 1024 (Lean.Parser.symbol "break"))

source

def Lean.Parser.Term.doContinue :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doContinue = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doContinue" (some `Lean.Parser.Term.doContinue)) (Lean.Parser.leadingNode `Lean.Parser.Term.doContinue 1024 (Lean.Parser.symbol "continue"))

source

def Lean.Parser.Term.doReturn :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doReturn = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doReturn" (some `Lean.Parser.Term.doReturn)) (Lean.Parser.leadingNode `Lean.Parser.Term.doReturn Lean.Parser.leadPrec (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "return ") fun x => Lean.Parser.optional (HAndThen.hAndThen Lean.Parser.checkLineEq fun x => Lean.Parser.termParser))))

source

def Lean.Parser.Term.doDbgTrace :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doDbgTrace = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doDbgTrace" (some `Lean.Parser.Term.doDbgTrace)) (Lean.Parser.leadingNode `Lean.Parser.Term.doDbgTrace Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "dbg_trace ") fun x => HOrElse.hOrElse (Lean.Parser.interpolatedStr Lean.Parser.termParser) fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.doAssert :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doAssert = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doAssert" (some `Lean.Parser.Term.doAssert)) (Lean.Parser.leadingNode `Lean.Parser.Term.doAssert Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "assert! ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.doExpr :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doExpr = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doExpr" (some `Lean.Parser.Term.doExpr)) (Lean.Parser.leadingNode `Lean.Parser.Term.doExpr 1024 (HAndThen.hAndThen Lean.Parser.Term.notFollowedByRedefinedTermToken fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => Lean.Parser.notFollowedBy (HOrElse.hOrElse (Lean.Parser.symbol ":=") fun x => HOrElse.hOrElse (Lean.Parser.symbol "←") fun x => Lean.Parser.symbol "<-") "unexpected token after 'expr' in 'do' block"))

source

def Lean.Parser.Term.doNested :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doNested = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doNested" (some `Lean.Parser.Term.doNested)) (Lean.Parser.leadingNode `Lean.Parser.Term.doNested 1024 (HAndThen.hAndThen (Lean.Parser.symbol "do ") fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Term.do :

Lean.Parser.Parser

Equations

Lean.Parser.Term.do = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "do" (some `Lean.Parser.Term.do)) (Lean.Parser.leadingNode `Lean.Parser.Term.do Lean.Parser.argPrec (HAndThen.hAndThen Lean.Parser.ppAllowUngrouped fun x => HAndThen.hAndThen (Lean.Parser.symbol "do ") fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Term.doElem.quot :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doElem.quot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quot" (some `Lean.Parser.Term.doElem.quot)) (Lean.Parser.leadingNode `Lean.Parser.Term.doElem.quot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(doElem|") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth Lean.Parser.doElemParser) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.termUnless :

Lean.Parser.Parser

Equations

Lean.Parser.Term.termUnless = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "termUnless" (some `Lean.Parser.Term.termUnless)) (Lean.Parser.leadingNode `Lean.Parser.Term.termUnless 1024 (HAndThen.hAndThen (Lean.Parser.symbol "unless ") fun x => HAndThen.hAndThen (Lean.Parser.withForbidden "do" Lean.Parser.termParser) fun x => HAndThen.hAndThen (Lean.Parser.symbol "do ") fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Term.termFor :

Lean.Parser.Parser

Equations

Lean.Parser.Term.termFor = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "termFor" (some `Lean.Parser.Term.termFor)) (Lean.Parser.leadingNode `Lean.Parser.Term.termFor 1024 (HAndThen.hAndThen (Lean.Parser.symbol "for ") fun x => HAndThen.hAndThen (Lean.Parser.sepBy1 Lean.Parser.Term.doForDecl ", " (Lean.Parser.symbol ", ")) fun x => HAndThen.hAndThen (Lean.Parser.symbol "do ") fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Term.termTry :

Lean.Parser.Parser

Equations

Lean.Parser.Term.termTry = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "termTry" (some `Lean.Parser.Term.termTry)) (Lean.Parser.leadingNode `Lean.Parser.Term.termTry 1024 (HAndThen.hAndThen (Lean.Parser.symbol "try ") fun x => HAndThen.hAndThen Lean.Parser.Term.doSeq fun x => HAndThen.hAndThen (Lean.Parser.many (HOrElse.hOrElse Lean.Parser.Term.doCatch fun x => Lean.Parser.Term.doCatchMatch)) fun x => Lean.Parser.optional Lean.Parser.Term.doFinally))

source

def Lean.Parser.Term.termReturn :

Lean.Parser.Parser

Equations

Lean.Parser.Term.termReturn = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "termReturn" (some `Lean.Parser.Term.termReturn)) (Lean.Parser.leadingNode `Lean.Parser.Term.termReturn Lean.Parser.leadPrec (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "return ") fun x => Lean.Parser.optional (HAndThen.hAndThen Lean.Parser.checkLineEq fun x => Lean.Parser.termParser))))