fix: sorry-out alignment goals in benchmark

leanprover · Sep 26, 2024 · 1c56f0e · 1c56f0e
1 parent 1f948b8
commit 1c56f0e
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 0 deletions.
diff --git a/Benchmarks/SHA512_150.lean b/Benchmarks/SHA512_150.lean
@@ -13,4 +13,5 @@ benchmark sha512_150_instructions : SHA512Bench 150 := fun s0 _ h => by
   intros
   sym_n 150
   simp only [h, bitvec_rules]
+  · exact (sorry : Aligned ..)
   done
diff --git a/Benchmarks/SHA512_225.lean b/Benchmarks/SHA512_225.lean
@@ -13,4 +13,5 @@ benchmark sha512_225_instructions : SHA512Bench 225 := fun s0 _ h => by
   intros
   sym_n 225
   simp only [h, bitvec_rules]
+  · exact (sorry : Aligned ..)
   done
diff --git a/Benchmarks/SHA512_400.lean b/Benchmarks/SHA512_400.lean
@@ -13,4 +13,5 @@ benchmark sha512_400_instructions : SHA512Bench 400 := fun s0 _ h => by
   intros
   sym_n 400
   simp only [h, bitvec_rules]
+  · exact (sorry : Aligned ..)
   done