Documentation

Lean.Parser.Syntax

source
@[inline]
def Lean.Parser.precedenceParser (rbp : optParam Nat 0) :
Lean.Parser.Parser
Equations
source
@[inline]
def Lean.Parser.syntaxParser (rbp : optParam Nat 0) :
Lean.Parser.Parser
Equations
source
def Lean.Parser.precedence:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.optPrecedence:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Syntax.numPrec:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Syntax.paren:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Syntax.cat:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Syntax.unary:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Syntax.binary:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Syntax.sepBy:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Syntax.sepBy1:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Syntax.atom:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Syntax.nonReserved:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.stx.quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.prec.quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.prio.quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.namedName:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.optNamedName:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Command.prefix:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.infix:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.infixl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.infixr:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.postfix:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.mixfixKind:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.mixfix:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.identPrec:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.optKind:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.notationItem:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.notation:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.macro_rules:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.syntax:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.syntaxAbbrev:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.catBehaviorBoth:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.catBehaviorSymbol:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.catBehavior:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.syntaxCat:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.macroArg:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.macroRhs (quotP : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.macroTailTactic:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.macroTailCommand:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.macroTailDefault:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.macroTail:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.macro:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.elab_rules:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.elabArg:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Command.elabTail:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.elab:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.