Documentation

Lean.Parser.Attr

@[inline]

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

Lean.Parser.Parser

Equations

Lean.Parser.priorityParser rbp = Lean.Parser.categoryParser `prio rbp

@[inline]

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

Lean.Parser.Parser

Equations

Lean.Parser.attrParser rbp = Lean.Parser.categoryParser `attr rbp

def Lean.Parser.Priority.numPrio:

Lean.Parser.Parser

Equations

Lean.Parser.Priority.numPrio = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.numLit

def Lean.Parser.Attr.simple:

Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.macro:

Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.export:

Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.recursor:

Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.class:

Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.instance:

Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.defaultInstance:

Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.externEntry:

Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.extern:

Lean.Parser.Parser

Equations

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