chore: fix bug in omega (#4184)

Fixes #4183
leanprover · May 15, 2024 · f636168 · f636168
1 parent 9a8e7a6
commit f636168
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git 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
@@ -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 `<`