From 7ae8b4d170ecf83e0fed12c8e7f81f32e8159070 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 25 Sep 2024 13:55:04 -0500 Subject: [PATCH] chore: suppress warning about state in the benchmarks The name for `s0` was previously inaccessible, which tripped up the `inferStatePrefixAndNumber` warning --- Benchmarks/SHA512_150.lean | 3 +-- Benchmarks/SHA512_225.lean | 3 +-- Benchmarks/SHA512_400.lean | 3 +-- 3 files changed, 3 insertions(+), 6 deletions(-) diff --git a/Benchmarks/SHA512_150.lean b/Benchmarks/SHA512_150.lean index f106c2e3..b54d8f83 100644 --- 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 index 39cd0370..26310030 100644 --- 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 index 2300c0db..bd725f6f 100644 --- 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