From 57bed748710658efecd1ee05885129a06ffce7bd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 17 Sep 2020 08:15:28 -0700
Subject: [PATCH] chore: add `Rewrite.lean`

---
 src/Lean/Elab/Tactic.lean         |  1 +
 src/Lean/Elab/Tactic/Rewrite.lean | 21 +++++++++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 src/Lean/Elab/Tactic/Rewrite.lean

diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean
index 5c244d087d..3576fc8576 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@@ -11,3 +11,4 @@ import Lean.Elab.Tactic.Generalize
 import Lean.Elab.Tactic.Injection
 import Lean.Elab.Tactic.Match
 import Lean.Elab.Tactic.Binders
+import Lean.Elab.Tactic.Rewrite
diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
new file mode 100644
index 0000000000..8bd4a58e15
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.ElabTerm
+
+namespace Lean
+namespace Elab
+namespace Tactic
+
+@[builtinMacro Lean.Parser.Tactic.rewriteSeq] def expandRewriteTactic : Macro :=
+fun stx => throw $ Macro.Exception.error stx "WIP"
+
+@[builtinTactic «rewrite»] def evalRewrite : Tactic :=
+fun stx => throwError "WIP"
+
+end Tactic
+end Elab
+end Lean