From f63616891fd3c9888ec1844f0744985bcb631a1e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 16 May 2024 08:21:17 +1000 Subject: [PATCH] chore: fix bug in omega (#4184) Fixes #4183 --- src/Lean/Elab/Tactic/Omega/OmegaM.lean | 2 +- tests/lean/run/omega.lean | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Tactic/Omega/OmegaM.lean b/src/Lean/Elab/Tactic/Omega/OmegaM.lean index 091843360645..e82ba2723bcc 100644 --- a/src/Lean/Elab/Tactic/Omega/OmegaM.lean +++ b/src/Lean/Elab/Tactic/Omega/OmegaM.lean @@ -150,7 +150,7 @@ partial def groundInt? (e : Expr) : Option Int := | _, _ => none | _ => e.int? where op (f : Int → Int → Int) (x y : Expr) : Option Int := - match groundNat? x, groundNat? y with + match groundInt? x, groundInt? y with | some x', some y' => some (f x' y') | _, _ => none diff --git a/tests/lean/run/omega.lean b/tests/lean/run/omega.lean index 262ecfe2e06e..0ed9fd7c8ff9 100644 --- a/tests/lean/run/omega.lean +++ b/tests/lean/run/omega.lean @@ -382,6 +382,10 @@ example (x : Nat) : x < 2 → (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2) ∧ (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2 → x < 3) := by omega +-- Reported in Lean FRO office hours 2024-05-16 by Michael George +example (s : Int) (s0 : s < (0 : Int)) : 63 + (s - 2 ^ 63) ≤ 62 - 2 ^ 63 := by + omega + /-! ### Fin -/ -- Test `<`