From 2eb76580f144ed783c47c48b0923944eb138fe0d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 11 Nov 2020 16:39:01 -0800
Subject: [PATCH] feat: add notation for `coe`

---
 src/Init/Coe.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index 9569470398..3adc4a8307 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -55,6 +55,8 @@ abbrev coeTC {α : Sort u} {β : Sort v} [CoeTC α β] (a : α) : β :=
 abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β :=
   CoeT.coe a
 
+prefix:max "↑" => coe
+
 abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a :=
   CoeFun.coe a