shorten Lawful.toPoised

opencompl · Sep 23, 2024 · 69aef1d · 69aef1d
1 parent e2816b7
commit 69aef1d
Showing 1 changed file with 2 additions and 8 deletions.
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -625,14 +625,8 @@ def DivModState.wr_lt_w {qr : DivModState w} (h : qr.Poised wr wn n d) : wr < w
 /-- If we have extra bits to spare in `n`,
 then we know the div mod state is poised to run another round of the shift subtractor. -/
 def DivModState.Lawful.toPoised {qr : DivModState w}
-    (h : qr.Lawful w wr (wn + 1) n d) : qr.Poised wr (wn + 1) n d where
-  hwrn := by have := h.hwrn; omega
-  hdPos := h.hdPos
-  hrLtDivisor := h.hrLtDivisor
-  hrWidth := h.hrWidth
-  hqWidth := h.hqWidth
-  hdiv := h.hdiv
-  hwn_lt := by omega
+    (h : qr.Lawful w wr (wn + 1) n d) : qr.Poised wr (wn + 1) n d :=
+  { h with hwn_lt := by omega }
 
 /-! ### Division shift subtractor -/