chore: suppress warning about state in the benchmarks

The name for `s0` was previously inaccessible, which tripped up the `inferStatePrefixAndNumber` warning
leanprover · Sep 25, 2024 · 7ae8b4d · 7ae8b4d
1 parent a22345b
commit 7ae8b4d
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 6 deletions.
diff --git a/Benchmarks/SHA512_150.lean b/Benchmarks/SHA512_150.lean
@@ -9,8 +9,7 @@ import Benchmarks.SHA512
 
 open Benchmarks
 
-benchmark sha512_150_instructions : SHA512Bench 150 := by
-  unfold SHA512Bench
+benchmark sha512_150_instructions : SHA512Bench 150 := fun s0 => by
   intros
   sym_n 150
   done
diff --git a/Benchmarks/SHA512_225.lean b/Benchmarks/SHA512_225.lean
@@ -9,8 +9,7 @@ import Benchmarks.SHA512
 
 open Benchmarks
 
-benchmark sha512_225_instructions : SHA512Bench 225 := by
-  unfold SHA512Bench
+benchmark sha512_225_instructions : SHA512Bench 225 := fun s0 => by
   intros
   sym_n 225
   done
diff --git a/Benchmarks/SHA512_400.lean b/Benchmarks/SHA512_400.lean
@@ -9,8 +9,7 @@ import Benchmarks.Command
 
 open Benchmarks
 
-benchmark sha512_400_instructions : SHA512Bench 400 := by
-  unfold SHA512Bench
+benchmark sha512_400_instructions : SHA512Bench 400 := fun s0 => by
   intros
   sym_n 400
   done