From 611c77f7e90b705294b0e7e34fd736894eee24ee Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Oct 2020 10:18:50 -0700 Subject: [PATCH] chore: move file to new frontend --- src/Lean/Elab/Tactic/Binders.lean | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/src/Lean/Elab/Tactic/Binders.lean b/src/Lean/Elab/Tactic/Binders.lean index 295156ff12..bdad0da0d1 100644 --- a/src/Lean/Elab/Tactic/Binders.lean +++ b/src/Lean/Elab/Tactic/Binders.lean @@ -4,18 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Elab.Tactic.Basic - -namespace Lean -namespace Elab -namespace Tactic +new_frontend +namespace Lean.Elab.Tactic private def liftTermBinderSyntax : Macro := fun stx => do - hole ← `(?_); + let hole ← `(?_) match stx.getKind with | Name.str (Name.str p "Tactic" _) s _ => - let kind := mkNameStr (mkNameStr p "Term") s; - let termStx := Syntax.node kind (stx.getArgs ++ #[mkAtomFrom stx "; ", hole]); + let kind := mkNameStr (mkNameStr p "Term") s + let termStx := Syntax.node kind (stx.getArgs ++ #[mkAtomFrom stx "; ", hole]) `(tactic| refine $termStx) | _ => Macro.throwError stx "unexpected binder syntax" @@ -26,9 +24,7 @@ fun stx => do @[builtinMacro Lean.Parser.Tactic.show] def expandShowTactic : Macro := fun stx => - let type := stx.getArg 1; + let type := stx.getArg 1 `(tactic| refine (show $type from ?_)) -end Tactic -end Elab -end Lean +end Lean.Elab.Tactic