feat: add tacticSeq

@Kha This is a small hack to allow users to use `tacticSeq` in
`syntax` command. Example:
```
syntax "repeat" tacticSeq : tactic
```
This commit is contained in:
Leonardo de Moura 2020-11-03 10:01:18 -08:00
parent f20a4244e4
commit 7654fa34e0

View file

@ -9,6 +9,10 @@ namespace Lean
namespace Parser
namespace Tactic
-- Auxiliary parsing category just to expose the nonterminal `tacticSeq` to the `syntax` command
builtin_initialize
registerBuiltinParserAttribute `builtinTacticSeqParser `tacticSeq
def underscoreFn : ParserFn := fun c s =>
let s := symbolFn "_" c s;
let stx := s.stxStack.back;