From 8630d78b3fcaaa6dd6bd387e5f3d7d0983d1ca90 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 24 Aug 2020 13:55:14 +0200 Subject: [PATCH] fix: Int.add spec --- src/Init/Data/Int/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 2de502f03e..530bc98332 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -52,7 +52,7 @@ match m, n with | ofNat m, ofNat n => ofNat (m + n) | ofNat m, negSucc n => subNatNat m (succ n) | negSucc m, ofNat n => subNatNat n (succ m) -| negSucc m, negSucc n => negSucc (m + n) +| negSucc m, negSucc n => negSucc (succ (m + n)) @[extern "lean_int_mul"] protected def mul (m n : @& Int) : Int :=