From d8a548fe512de3ab6381c964d2dfb6b6f54fcf54 Mon Sep 17 00:00:00 2001 From: Adrien Champion Date: Mon, 10 Jul 2023 15:17:01 +0200 Subject: [PATCH] chore: fix `Int.div` docstring examples --- src/Init/Data/Int/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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. -/