Merge branch 'upstream-div-alt' of https://github.com/opencompl/lean4 …

…into upstream-div-alt
opencompl · Sep 24, 2024 · 2ba45c9 · 2ba45c9
2 parents 84dfd6a + 2839738
commit 2ba45c9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -690,7 +690,7 @@ private theorem two_mul_add_sub_lt_of_lt_of_lt_two (h : a < x) (hy : y < 2) :
 
 /-- We show that the output of `divSubtractShift` is lawful, which tells us that it
 obeys the division equation. -/
-def lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) :
+theorem lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) :
     DivModState.Lawful args (divSubtractShift args qr) := by
   rcases args with ⟨n, d⟩
   simp only [divSubtractShift, decide_eq_true_eq]