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

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

source

def Lean.Parser.Term.doSeqItem:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doSeqIndent:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doSeqBracketed:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doSeq:

Lean.Parser.Parser

Equations

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

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

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

source

def Lean.Parser.Term.doLet:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doLetElse:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doLetRec:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doIdDecl:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doPatDecl:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doLetArrow:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.letIdDeclNoBinders:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doReassign:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doReassignArrow:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doHave:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.elseIf:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doIfLetPure:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doIfLetBind:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doIfLet:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doIfProp:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doIfCond:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doIf:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doUnless:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doForDecl:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doFor:

Lean.Parser.Parser

Equations

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

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.doMatch:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doCatch:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doCatchMatch:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doFinally:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doTry:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doBreak:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doContinue:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doReturn:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doDbgTrace:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doAssert:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doExpr:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doNested:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.do:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.doElem.quot:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.termUnless:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.termFor:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.termTry:

Lean.Parser.Parser

Equations

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

source

def Lean.Parser.Term.termReturn:

Lean.Parser.Parser

Equations

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