Documentation
Lean
.
Parser
.
Level
Search
return to top
source
Imports
Lean.Parser.Extra
Imported by
Lean
.
Parser
.
levelParser
Lean
.
Parser
.
Level
.
paren
Lean
.
Parser
.
Level
.
max
Lean
.
Parser
.
Level
.
imax
Lean
.
Parser
.
Level
.
hole
Lean
.
Parser
.
Level
.
num
Lean
.
Parser
.
Level
.
ident
Lean
.
Parser
.
Level
.
addLit
source
@[inline]
def
Lean
.
Parser
.
levelParser
(
rbp
:
Nat
:=
0
)
:
Parser
Equations
Instances For
source
def
Lean
.
Parser
.
Level
.
paren
:
Parser
Equations
Instances For
source
def
Lean
.
Parser
.
Level
.
max
:
Parser
Equations
Instances For
source
def
Lean
.
Parser
.
Level
.
imax
:
Parser
Equations
Instances For
source
def
Lean
.
Parser
.
Level
.
hole
:
Parser
Equations
Instances For
source
def
Lean
.
Parser
.
Level
.
num
:
Parser
Equations
Instances For
source
def
Lean
.
Parser
.
Level
.
ident
:
Parser
Equations
Instances For
source
def
Lean
.
Parser
.
Level
.
addLit
:
TrailingParser
Equations
Instances For