diff --git a/library/init/lean/parser/level.lean b/library/init/lean/parser/level.lean index 1b6c7fb287..b7a888a114 100644 --- a/library/init/lean/parser/level.lean +++ b/library/init/lean/parser/level.lean @@ -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 diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index ca7faf17c2..effb473551 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -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 -/