max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: increase runtime of "sigma iterator" benchmark (#11336)

Browse source 
This PR makes the "sigma iterator" benchmark more compute-intensive
because it was too fast and therefore flaky.
This commit is contained in:
Paul Reichert 2025-11-24 13:21:27 +01:00 • committed by GitHub
parent 54a10f0790
commit 6da35eeccb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/bench/sigmaIterator.lean
View file

@ -180,7 +180,7 @@ def f._at_.g.spec_0._redArg _x.1 _x.2 _x.3 it : Nat :=
```
-/
def g : Nat := Id.run do
(*...2000000).iter.filter (fun _ => True)
(*...30000000).iter.filter (fun _ => True)
|>.sigma (α := fun _ => _) (param := 0)
|> f (acc := 0)