From f7deabfd194c12909645b428c8b3194e62f54005 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Nov 2014 19:02:11 -0800
Subject: [PATCH] feat(library/rename): add notation for `rename`

---
 library/tools/tactic.lean      |  2 ++
 tests/lean/run/rename_tac.lean | 10 +++++++++-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean
index 707d36746..39d6b5e34 100644
--- a/library/tools/tactic.lean
+++ b/library/tools/tactic.lean
@@ -58,6 +58,8 @@ opaque definition unfold     (e : expr)   : tactic := builtin
 opaque definition exact      (e : expr)   : tactic := builtin
 opaque definition trace      (s : string) : tactic := builtin
 
+notation a `↦` b := rename a b
+
 inductive expr_list : Type :=
 nil  : expr_list,
 cons : expr → expr_list → expr_list
diff --git a/tests/lean/run/rename_tac.lean b/tests/lean/run/rename_tac.lean
index 9db0f1857..c9d5834d3 100644
--- a/tests/lean/run/rename_tac.lean
+++ b/tests/lean/run/rename_tac.lean
@@ -1,10 +1,18 @@
 import tools.tactic logic
 open tactic
 
-theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
+theorem foo1 (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
 begin
   apply eq.trans,
   rename Hab Foo,
   apply Foo,
   apply Hbc,
 end
+
+theorem foo2 (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c :=
+begin
+  apply eq.trans,
+  Hab ↦ Foo,
+  apply Foo,
+  apply Hbc,
+end