We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent a753952 commit a75b330Copy full SHA for a75b330
src/Init/Data/BitVec/Bitblast.lean
@@ -2510,6 +2510,7 @@ theorem aux1 {x : BitVec w} (hw : 1 < w) (hk : 0 < k) (hk' : k < w) : -- at leas
2510
theorem aux2 {x y : BitVec w} (hw : 1 < w) :
2511
clz x + clz y ≤ w - 2 → resRec x y (w - 1) (by omega) (by omega) (by omega) := by sorry
2512
2513
+
2514
theorem aux3 {x y : BitVec w} (hw : 1 < w) :
2515
resRec x y (w - 1) (by sorry) (by sorry) (by sorry) → clz x + clz y ≤ w - 2 := by sorry
2516
0 commit comments