Documentation
Lean
.
Parser
.
Attr
Search
Google site search
Lean
.
Parser
.
Attr
source
Imports
Init
Lean.Parser.Basic
Lean.Parser.Extra
Imported by
Lean
.
Parser
.
priorityParser
Lean
.
Parser
.
attrParser
Lean
.
Parser
.
Priority
.
numPrio
Lean
.
Parser
.
Attr
.
simple
Lean
.
Parser
.
Attr
.
macro
Lean
.
Parser
.
Attr
.
export
Lean
.
Parser
.
Attr
.
recursor
Lean
.
Parser
.
Attr
.
class
Lean
.
Parser
.
Attr
.
instance
Lean
.
Parser
.
Attr
.
default_instance
Lean
.
Parser
.
Attr
.
specialize
Lean
.
Parser
.
Attr
.
externEntry
Lean
.
Parser
.
Attr
.
extern
source
@[inline]
def
Lean
.
Parser
.
priorityParser
(rbp :
optParam
Nat
0
)
:
Lean.Parser.Parser
Instances For
source
@[inline]
def
Lean
.
Parser
.
attrParser
(rbp :
optParam
Nat
0
)
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Priority
.
numPrio
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
simple
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
macro
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
export
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
recursor
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
class
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
instance
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
default_instance
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
specialize
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
externEntry
:
Lean.Parser.Parser
Instances For
source
def
Lean
.
Parser
.
Attr
.
extern
:
Lean.Parser.Parser
Instances For