From 83c2e8bf754c78e6893a43ff566c6c5bf6ab39ef Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 20 Sep 2021 11:53:40 +0200 Subject: [PATCH] feat: expose `many(1)Indent` as parser aliases --- src/Lean/Parser.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index 21bc210d21..8870b26c74 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -33,6 +33,8 @@ builtin_initialize register_parser_alias "atomic" atomic register_parser_alias "many" many register_parser_alias "many1" many1 + register_parser_alias "manyIndent" manyIndent + register_parser_alias "many1Indent" many1Indent register_parser_alias "optional" optional register_parser_alias "withPosition" withPosition register_parser_alias "interpolatedStr" interpolatedStr