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

chore: prepare to move ParserKind

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-30 19:41:16 -08:00
parent b439de68a5
commit a1f079227b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Parser/Parser.lean
View file

@ -1461,7 +1461,7 @@ registerAttribute {
match decl.type with
| Expr.const `Lean.Parser.TrailingParser _ _ =>
declareTrailingBuiltinParser env refDeclName declName
| Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.Parser.ParserKind.leading _ _) _ =>
| Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ =>
declareLeadingBuiltinParser env refDeclName declName
| _ =>
throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))