diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index b932785795..8710da9bb5 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -269,8 +269,8 @@ def natAbs (m : @& Int) : Nat := #eval (12 : Int) / (7 : Int) -- 1 #eval (12 : Int) / (-7 : Int) -- -1 - #eval (-12 : Int) / (7 : Int) -- -2 - #eval (-12 : Int) / (-7 : Int) -- 2 + #eval (-12 : Int) / (7 : Int) -- -1 + #eval (-12 : Int) / (-7 : Int) -- 1 ``` Implemented by efficient native code. -/