From d6671db6b002aa03cc89eabf259ba247cd140796 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 5 Dec 2024 22:47:24 +0000 Subject: [PATCH] fix bad comments --- Mathlib/Data/Rat/Floor.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Rat/Floor.lean b/Mathlib/Data/Rat/Floor.lean index fbba4707039b82..a916bde474c7d1 100644 --- a/Mathlib/Data/Rat/Floor.lean +++ b/Mathlib/Data/Rat/Floor.lean @@ -142,7 +142,7 @@ def evalIntFloor : NormNumExt where eval {u αZ} e := do let _i ← synthInstanceQ q(LinearOrderedField $α) assertInstancesCommute have z : Q(ℤ) := mkRawIntLit ⌊q⌋ - letI : $z =Q ⌊$n / $d⌋ := ⟨⟩ + letI : $z =Q $n / $d := ⟨⟩ return .isInt q(inferInstance) z ⌊q⌋ q(isInt_intFloor_ofIsRat _ $n $d $h) | _, _, _ => failure @@ -172,7 +172,7 @@ def evalIntCeil : NormNumExt where eval {u αZ} e := do return .isNat q(inferInstance) _ q(isNat_intCeil $x _ $pb) | .isNegNat _ _ pb => do assertInstancesCommute - -- floor always keeps naturals negative, so we can shortcut `.isInt` + -- ceil always keeps naturals negative, so we can shortcut `.isInt` return .isNegNat q(inferInstance) _ q(isInt_intCeil _ _ $pb) | .isRat _ q n d h => do let _i ← synthInstanceQ q(LinearOrderedField $α)