fix: remove now-redundant simp from benchmarks

leanprover · Oct 1, 2024 · 6fecfdb · 6fecfdb
1 parent b95fe25
commit 6fecfdb
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 3 deletions.
diff --git a/Benchmarks/SHA512_150.lean b/Benchmarks/SHA512_150.lean
@@ -12,6 +12,5 @@ open Benchmarks
 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
@@ -12,6 +12,5 @@ open Benchmarks
 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
@@ -12,6 +12,5 @@ open Benchmarks
 benchmark sha512_400_instructions : SHA512Bench 400 := fun s0 _ h => by
   intros
   sym_n 400
-  simp only [h, bitvec_rules]
   · exact (sorry : Aligned ..)
   done