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

chore: prepare for refactoring

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-30 20:41:10 -08:00
parent 54bdddb98f
commit 6b1e64d7ea
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1733,6 +1733,9 @@ match env.find? constName with
| Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ => do
p ← env.evalConst (Parser leading) constName;
pure ⟨leading, p⟩
| Expr.const `Lean.Parser.Parser _ _ => do
p ← env.evalConst (Parser leading) constName;
pure ⟨leading, p⟩
| Expr.const `Lean.ParserDescr _ _ => do
d ← env.evalConst ParserDescr constName;
p ← compileParserDescr categories d;
@ -1897,6 +1900,8 @@ match env.find? declName with
declareTrailingBuiltinParser env catName declName
| Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ =>
declareLeadingBuiltinParser env catName declName
| Expr.const `Lean.Parser.Parser _ _ =>
declareLeadingBuiltinParser env catName declName
| _ =>
throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))