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

feat: parser alias for tacticSeqIndentGt

Browse source
This commit is contained in:
Sebastian Ullrich 2023-03-15 10:54:05 +01:00
parent d7a0197fee
commit a89accfbbe
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Parser/Tactic.lean
View file

@ -11,6 +11,7 @@ namespace Tactic
builtin_initialize
register_parser_alias tacticSeq
register_parser_alias tacticSeqIndentGt
/- This is a fallback tactic parser for any identifier which exists only
to improve syntax error messages.