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

chore: adjust code

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-28 14:28:12 -07:00
parent 3f12066136
commit b9104d069e
1 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -246,6 +246,15 @@ modifyMCtx fun mctx =>
@[builtinTactic seq] def evalSeq : Tactic :=
fun stx => (stx.getArg 0).forSepArgsM evalTactic
@[builtinTactic paren] def evalParen : Tactic :=
fun stx => evalTactic (stx.getArg 1)
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic
@[builtinTactic tacticSeq] def evalTacticSeq : Tactic :=
fun stx => evalTactic (stx.getArg 0)
partial def evalChoiceAux (tactics : Array Syntax) : Nat → TacticM Unit
| i =>
if h : i < tactics.size then
@ -376,12 +385,6 @@ fun stx => match_syntax stx with
| `(tactic| subst $hs*) => forEachVar hs Meta.subst
| _ => throwUnsupportedSyntax
@[builtinTactic paren] def evalParen : Tactic :=
fun stx => evalTactic (stx.getArg 1)
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic :=
fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic
/--
First method searches for a metavariable `g` s.t. `tag` is a suffix of its name.
If none is found, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/