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

fix: evalTacticSeqBracketed and evalSeq1

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-06 08:06:11 -07:00
parent 76a8f17c4b
commit 71e6ab2a06
1 changed files with 11 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -242,22 +242,21 @@ modifyMCtx fun mctx =>
(mctx, 1);
mctx
def evalSeq : Tactic :=
fun stx => (stx.getArg 0).forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
@[builtinTactic seq1] def evalSeq1 : Tactic := evalSeq
@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := evalSeq
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic
@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic :=
fun stx => focus $ evalTactic (stx.getArg 1)
@[builtinTactic seq1] def evalSeq1 : Tactic :=
fun stx => (stx.getArg 0).forSepArgsM evalTactic
@[builtinTactic paren] def evalParen : Tactic :=
fun stx => evalSeq1 (stx.getArg 1)
@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic :=
fun stx => (stx.getArg 0).forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forArgsM fun seqElem => evalTactic (seqElem.getArg 0)
@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic :=
fun stx => focus $ evalTactic (stx.getArg 1)
@[builtinTactic tacticSeq] def evalTacticSeq : Tactic :=
fun stx => evalTactic (stx.getArg 0)