Found another theorem that is already proven

opencompl · Nov 13, 2023 · e33817c · e33817c
1 parent 1fc339f
commit e33817c
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean
@@ -378,7 +378,7 @@ theorem bitvec_229 :
 theorem bitvec_239 :
  ∀ (w : Nat) (Y X : BitVec w), (0 - X) * (0 - Y) = X * Y
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_275:
  ∀ (Y X : BitVec 5),

diff --git a/lakefile.olean b/lakefile.olean