Bugfix for norm num when testing divisibility of integers (#2355)

they were assumed nats somehow Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
leanprover-community · Apr 9, 2020 · e4e483e · e4e483e
1 parent c3d9cf9
commit e4e483e
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/src/tactic/norm_num.lean b/src/tactic/norm_num.lean
@@ -295,7 +295,10 @@ meta def eval_div_ext (simp : expr → tactic (expr × expr)) : expr → tactic
   | _ := failed
   end,
   p₁ ← mk_app ``propext [@expr.const tt n [] e₁ e₂],
-  (e', p₂) ← simp `(%%e₂ % %%e₁ = 0),
+  (c, el) ← c.mk_app ``has_mod.mod [e₂, e₁],
+  (c, z) ← c.mk_app ``has_zero.zero [],
+  e ← mk_app ``eq [el, z],
+  (e', p₂) ← simp e,
   p' ← mk_eq_trans p₁ p₂,
   return (e', p')
 | _ := failed

diff --git a/test/norm_num.lean b/test/norm_num.lean
@@ -42,3 +42,6 @@ example (x : ℕ) : ℕ := begin
   let n : ℕ, {apply_normed (2^32 - 71)},
   exact n
 end
+
+
+example (h : (5 : ℤ) ∣ 2) : false := by norm_num at h