From 2192e6148babe0aec470a3a0110a636ae4ea4bfc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Jan 2022 15:16:03 -0800
Subject: [PATCH] chore: remove `coe`, `coeSort`, and `coeFun` abbreviations
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The notation `↑ e` is now expanded eagerly.

See #403
---
 src/Init/Coe.lean                     | 29 +++++++--------------------
 src/Lean/Data/Json/Basic.lean         |  2 +-
 src/Lean/Meta/Coe.lean                |  2 --
 src/Lean/Server/FileWorker/Utils.lean |  2 +-
 4 files changed, 9 insertions(+), 26 deletions(-)

diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index 28cd794db9..bc269d3218 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -40,19 +40,7 @@ class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where
 class CoeSort (α : Sort u) (β : outParam (Sort v)) where
   coe : α → β
 
-abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β :=
-  CoeT.coe a
-
-syntax:max (name := coeNotation) "↑" term : term
-
-macro_rules -- TODO: delete after update stage0
-  | `(↑ $x) => `(CoeT.coe $x)
-
-abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a :=
-  CoeFun.coe a
-
-abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β :=
-  CoeSort.coe a
+syntax:max (name := coeNotation) "↑" term:max : term
 
 instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [Coe β δ] [CoeTC α β] : CoeTC α δ where
   coe a := Coe.coe (CoeTC.coe a : β)
@@ -96,10 +84,7 @@ instance coeSortToCoeTail [inst : CoeSort α β] : CoeTail α β where
   coe b := b = true
 
 instance boolToSort : CoeSort Bool Prop where
-  coe b := b
-
-@[inline] instance coeDecidableEq (x : Bool) : Decidable (coe x) :=
-  inferInstanceAs (Decidable (x = true))
+  coe b := b = true
 
 instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
   coe := decide p
@@ -114,17 +99,17 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α wh
 
 @[inline] def liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
   let a ← liftM x
-  pure (coe a)
+  pure (CoeT.coe a)
 
 @[inline] def coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β := do
   let a ← x
-  pure <| coe a
+  pure <| CoeT.coe a
 
 instance [CoeFun α β] (a : α) : CoeDep α a (β a) where
-  coe := coeFun a
+  coe := CoeFun.coe a
 
 instance [CoeFun α (fun _ => β)] : CoeTail α β  where
-  coe a := coeFun a
+  coe a := CoeFun.coe a
 
 instance [CoeSort α β] : CoeTail α β where
-  coe a := coeSort a
+  coe a := CoeSort.coe a
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 7ecab73c14..203258ce2b 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -100,7 +100,7 @@ protected def toString : JsonNumber → String
     let exp := if exp < 0 then exp else 0
     let e' := (10 : Int) ^ (e - exp.natAbs)
     let left := (m / e').repr
-    let right := e' + coe m % e'
+    let right := e' + ↑m % e'
       |>.repr.toSubstring.drop 1
       |>.dropRightWhile (fun c => c = '0')
       |>.toString
diff --git a/src/Lean/Meta/Coe.lean b/src/Lean/Meta/Coe.lean
index f134968f4b..d292fd3798 100644
--- a/src/Lean/Meta/Coe.lean
+++ b/src/Lean/Meta/Coe.lean
@@ -13,8 +13,6 @@ namespace Lean.Meta
   used to implement coercions.
 -/
 def isCoeDecl (declName : Name) : Bool :=
-  declName == ``coe  ||
-  declName == ``coeFun || declName == ``coeSort ||
   declName == ``Coe.coe || declName == ``CoeTC.coe || declName == ``CoeHead.coe ||
   declName == ``CoeTail.coe || declName == ``CoeHTCT.coe || declName == ``CoeDep.coe ||
   declName == ``CoeT.coe || declName == ``CoeFun.coe || declName == ``CoeSort.coe ||
diff --git a/src/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean
index 871a2744e7..7689647267 100644
--- a/src/Lean/Server/FileWorker/Utils.lean
+++ b/src/Lean/Server/FileWorker/Utils.lean
@@ -25,7 +25,7 @@ instance : Coe IO.Error ElabTaskError :=
   ⟨ElabTaskError.ioError⟩
 
 instance : MonadLift IO (EIO ElabTaskError) where
-  monadLift act := act.toEIO (coe ·)
+  monadLift act := act.toEIO (↑ ·)
 
 structure CancelToken where
   ref : IO.Ref Bool