/
Level.lean
38 lines (31 loc) · 1.08 KB
/
Level.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Lean.Parser.Extra
namespace Lean
namespace Parser
builtin_initialize
registerBuiltinParserAttribute `builtin_level_parser ``Category.level
@[inline] def levelParser (rbp : Nat := 0) : Parser :=
categoryParser `level rbp
namespace Level
@[builtin_level_parser] def paren := leading_parser
"(" >> withoutPosition levelParser >> ")"
@[builtin_level_parser] def max := leading_parser
nonReservedSymbol "max" true >> many1 (ppSpace >> levelParser maxPrec)
@[builtin_level_parser] def imax := leading_parser
nonReservedSymbol "imax" true >> many1 (ppSpace >> levelParser maxPrec)
@[builtin_level_parser] def hole := leading_parser
"_"
@[builtin_level_parser] def num :=
checkPrec maxPrec >> numLit
@[builtin_level_parser] def ident :=
checkPrec maxPrec >> Parser.ident
@[builtin_level_parser] def addLit := trailing_parser:65
" + " >> numLit
end Level
end Parser
end Lean