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

chore: fix benchmark added in #9380 (#9384)

Browse source
This commit is contained in:
Joachim Breitner 2025-07-15 20:24:34 +02:00 • committed by GitHub
parent aa6f22d102
commit 0926d27100
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/bench/simp-bubblesort-265.lean → tests/bench/simp_bubblesort_256.lean
View file

@ -24,7 +24,7 @@ axiom swap : f b (f a xs) = f a (f b xs)
axiom iter_zero : iter z g x = g x
axiom iter_succ : iter (s i) g x = iter i g (iter i g x)
noncomputable def steps : n := s (s (s (s (s (s (s z))))))
noncomputable def steps : N := s (s (s (s (s (s (s z))))))
set_option maxRecDepth 100000

4
tests/bench/speedcenter.exec.velcom.yaml
View file

@ -402,11 +402,11 @@
<<: *time
cmd: lean simp_arith1.lean
- attributes:
description: simp-bubblesort-265
description: simp_bubblesort_256
tags: [fast, suite]
run_config:
<<: *time
cmd: lean simp-bubblesort-265.lean
cmd: lean simp_bubblesort_256.lean
- attributes:
description: nat_repr
tags: [fast, suite]