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

feat: expose many(1)Indent as parser aliases

Browse source
This commit is contained in:
Sebastian Ullrich 2021-09-20 11:53:40 +02:00
parent f2a418a7ae
commit 83c2e8bf75
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser.lean
View file

@ -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