From 3a6d579bbb56c1ebdfab36e69b55c6eb7efb39b2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Sep 2020 12:32:22 -0700 Subject: [PATCH] feat: expand `rewriteSeq` macro --- src/Lean/Elab/Tactic/Rewrite.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index 8bd4a58e15..d4c45ae030 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -11,10 +11,15 @@ namespace Elab namespace Tactic @[builtinMacro Lean.Parser.Tactic.rewriteSeq] def expandRewriteTactic : Macro := -fun stx => throw $ Macro.Exception.error stx "WIP" +fun stx => + let seq := ((stx.getArg 1).getArg 1).getArgs.getSepElems; + let loc := stx.getArg 2; + pure $ mkNullNode $ seq.map fun rwRule => Syntax.node `Lean.Parser.Tactic.rewrite #[stx.getArg 0, rwRule, loc] @[builtinTactic «rewrite»] def evalRewrite : Tactic := -fun stx => throwError "WIP" +fun stx => do + logInfo $ "WIP " ++ stx; + pure () end Tactic end Elab