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

chore: add evalSeq1

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-28 15:26:35 -07:00
parent 23f7a4b435
commit fba1571fdf
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Tactic/Basic.lean
View file

@ -246,8 +246,10 @@ modifyMCtx fun mctx =>
@[builtinTactic seq] def evalSeq : Tactic :=
fun stx => (stx.getArg 0).forSepArgsM evalTactic
@[builtinTactic seq1] def evalSeq1 : Tactic := evalSeq
@[builtinTactic paren] def evalParen : Tactic :=
fun stx => evalTactic (stx.getArg 1)
fun stx => evalSeq1 (stx.getArg 1)
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic