From 338aa5aa7cf5eaef1da65687857fa3b8227de544 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Feb 2024 14:30:05 -0800 Subject: [PATCH] fix: `Std.BitVec` occurrences at `OmegaM.lean` --- src/Lean/Elab/Tactic/Omega/OmegaM.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Tactic/Omega/OmegaM.lean b/src/Lean/Elab/Tactic/Omega/OmegaM.lean index 5397e938e3..a73d859214 100644 --- a/src/Lean/Elab/Tactic/Omega/OmegaM.lean +++ b/src/Lean/Elab/Tactic/Omega/OmegaM.lean @@ -7,6 +7,7 @@ prelude import Init.Omega.LinearCombo import Init.Omega.Int import Init.Omega.Logic +import Init.Data.BitVec import Lean.Meta.AppBuilder /-! @@ -173,8 +174,8 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do r := r.insert (mkApp (.const ``Int.neg_le_natAbs []) x) | _, (``Fin.val, #[n, i]) => r := r.insert (mkApp2 (.const ``Fin.isLt []) n i) - | _, (`Std.BitVec.toNat, #[n, x]) => - r := r.insert (mkApp2 (.const `Std.BitVec.toNat_lt []) n x) + | _, (``BitVec.toNat, #[n, x]) => + r := r.insert (mkApp2 (.const ``BitVec.toNat_lt []) n x) | _, _ => pure () return r | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with