From 27292c4f604cd10bd8fcb4af8cdc9721c6c354af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Dec 2020 06:48:58 -0800
Subject: [PATCH] chore: prepare to change `OfNat` type class

---
 src/Lean/Elab/SyntheticMVars.lean              |  2 +-
 src/Lean/Elab/Term.lean                        | 11 ++---------
 src/Lean/Meta/Offset.lean                      |  6 +-----
 .../PrettyPrinter/Delaborator/Builtins.lean    | 18 ++----------------
 4 files changed, 6 insertions(+), 31 deletions(-)

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 07b1e0c3bb..49bb1f344c 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -180,7 +180,7 @@ private def synthesizeUsingDefaultPrio (prio : Nat) : TermElabM Bool := do
           return true
   /- Recall that s.syntheticMVars is essentially a stack. The first metavariable was the last one created.
      We want to apply the default instance in reverse creation order. Otherwise,
-     `toString 0` will produce a `OfNat String` cannot be synthesized error. -/
+     `toString 0` will produce a `OfNat String _` cannot be synthesized error. -/
   visit (← get).syntheticMVars.reverse []
 
 /--
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index af0e5408ee..53e7b45701 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1263,15 +1263,8 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL
   | _                 => pure ()
   let u ← getLevel typeMVar
   let u ← decLevel u
-  if val == 0 then
-    let mvar ← mkInstMVar (mkApp (Lean.mkConst `Zero [u]) typeMVar)
-    return mkApp2 (Lean.mkConst `Zero.zero [u]) typeMVar mvar
-  else if val == 1 then
-    let mvar ← mkInstMVar (mkApp (Lean.mkConst `One [u]) typeMVar)
-    return mkApp2 (Lean.mkConst `One.one [u]) typeMVar mvar
-  else
-    let mvar ← mkInstMVar (mkApp (Lean.mkConst `OfNat [u]) typeMVar)
-    return mkApp3 (Lean.mkConst `OfNat.ofNat [u]) typeMVar mvar (mkNatLit val)
+  let mvar ← mkInstMVar (mkApp2 (Lean.mkConst `OfNat [u]) typeMVar (mkNatLit val))
+  return mkApp3 (Lean.mkConst `OfNat.ofNat [u]) typeMVar (mkNatLit val) mvar
 
 @[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do
   match stx.isCharLit? with
diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean
index bd396cf987..0da0b32961 100644
--- a/src/Lean/Meta/Offset.lean
+++ b/src/Lean/Meta/Offset.lean
@@ -57,11 +57,7 @@ where
         let v₂ ← evalNat (e.getArg! 3)
         return v₁ * v₂
       else if c == `OfNat.ofNat && nargs == 3 then
-        evalNat (e.getArg! 2)
-      else if c == `One.one && nargs == 2 then
-        return 1
-      else if c == `Zero.zero && nargs == 2 then
-        return 0
+        evalNat (e.getArg! 1)
       else
         failure
     | _ => failure
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 6e117412f2..5881737949 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -349,26 +349,12 @@ def delabLit : Delab := do
   | Literal.natVal n => pure $ quote n
   | Literal.strVal s => pure $ quote s
 
--- `ofNat 0` ~> `0`
+-- `@OfNat.ofNat _ n _` ~> `n`
 @[builtinDelab app.OfNat.ofNat]
 def delabOfNat : Delab := whenPPOption getPPCoercions do
-  let e@(Expr.app _ (Expr.lit (Literal.natVal n) _) _) ← getExpr | failure
+  let (Expr.app (Expr.app _ (Expr.lit (Literal.natVal n) _) _) _ _) ← getExpr | failure
   return quote n
 
--- `One.one` ~> `1`
-@[builtinDelab app.One.one]
-def delabOne : Delab := whenPPOption getPPCoercions do
-  let e ← getExpr
-  guard <| e.getAppNumArgs == 2
-  return quote (1:Nat)
-
--- `Zero.zero` ~> `0`
-@[builtinDelab app.Zero.zero]
-def delabZero : Delab := whenPPOption getPPCoercions do
-  let e ← getExpr
-  guard <| e.getAppNumArgs == 2
-  return quote (0:Nat)
-
 /--
 Delaborate a projection primitive. These do not usually occur in
 user code, but are pretty-printed when e.g. `#print`ing a projection