max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/parser): minor

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-08 14:45:20 -07:00
parent f37cd3cd11
commit 95dc2c5ade
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/init/lean/parser/level.lean
View file

@ -15,8 +15,11 @@ constant builtinLevelParsingTable : IO.Ref ParsingTables := default _
@[init] def regBuiltinLevelParserAttr : IO Unit :=
registerBuiltinParserAttribute `builtinLevelParser `Lean.Parser.builtinLevelParsingTable
def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
{ fn := fun _ => runBuiltinParser "universe level" builtinLevelParsingTable rbp }
def levelParserFn {k : ParserKind} (rbp : Nat) : ParserFn k :=
fun _ => runBuiltinParser "universe level" builtinLevelParsingTable rbp
@[inline] def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
{ fn := levelParserFn rbp }
namespace Level

6
library/init/lean/parser/term.lean
View file

@ -16,9 +16,11 @@ constant builtinTermParsingTable : IO.Ref ParsingTables := default _
@[init] def regBuiltinTermParserAttr : IO Unit :=
registerBuiltinParserAttribute `builtinTermParser `Lean.Parser.builtinTermParsingTable
def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
{ fn := fun _ => runBuiltinParser "term" builtinTermParsingTable rbp }
def termParserFn {k : ParserKind} (rbp : Nat) : ParserFn k :=
fun _ => runBuiltinParser "term" builtinTermParsingTable rbp
@[inline] def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
{ fn := termParserFn rbp }
namespace Term
/- Helper functions for defining simple parsers -/