From e3e89b4945db2032e2976945cb9cf831dcd3784e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 16 Oct 2020 15:39:00 -0700 Subject: [PATCH] chore: add coercion for new frontend --- src/Init/Data/Int/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 62ef3c9387..7fb3619519 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -22,6 +22,7 @@ attribute [extern "lean_nat_to_int"] Int.ofNat attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc instance : HasCoe Nat Int := ⟨Int.ofNat⟩ +instance : Coe Nat Int := ⟨Int.ofNat⟩ namespace Int protected def zero : Int := ofNat 0