Remove the ToExpr Int instance

This instance exists upstream in core
leanprover-community · Oct 5, 2024 · c64bdcc · c64bdcc
1 parent 2c8ae45
commit c64bdcc
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/Qq/ForLean/ToExpr.lean b/Qq/ForLean/ToExpr.lean
@@ -2,12 +2,6 @@ import Lean
 
 open Lean
 
-instance : ToExpr Int where
-  toTypeExpr := .const ``Int []
-  toExpr i := match i with
-    | .ofNat n => mkApp (.const ``Int.ofNat []) (toExpr n)
-    | .negSucc n => mkApp (.const ``Int.negSucc []) (toExpr n)
-
 instance : ToExpr MVarId where
   toTypeExpr := .const ``MVarId []
   toExpr i := mkApp (.const ``MVarId.mk []) (toExpr i.name)