chore: ToExpr Int (#449)

leanprover-community · Dec 16, 2023 · ebdd969 · ebdd969
1 parent 9dd24a3
commit ebdd969
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/Std/Data/Int/Basic.lean b/Std/Data/Int/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Std.Classes.Dvd
+import Lean.ToExpr
 
 open Nat
 
@@ -164,3 +165,10 @@ protected def shiftRight : Int → Nat → Int
   | Int.negSucc n, s => Int.negSucc (n >>> s)
 
 instance : HShiftRight Int Nat Int := ⟨.shiftRight⟩
+
+open Lean in
+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)