chore: prepare to change OfNat type class

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 []
 
 /--

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

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

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