test: add a benchmark that is slow to elaborate (#5656)
Add an example Lean file that includes an unusually large definition that takes a long time to elaborate. It may be that it's difficult to process it more efficiently, but perhaps someone will discover a way to improve it if it's in the benchmark suite. Improved performance on this benchmark will likely make some program analysis and verification tasks within Lean more feasible. --------- Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This commit is contained in:
Aaron Tomb
GitHub
parent
c1143d9432
commit
45b1b367ca
2 changed files with 465 additions and 0 deletions
459
tests/bench/big_do.lean
Normal file
459
tests/bench/big_do.lean
Normal file
|
|
@ -0,0 +1,459 @@
|
|||
/-!
|
||||
This benchmark exercises
|
||||
* general elaboration, likely from many nested lambdas
|
||||
* code generation, ditto
|
||||
-/
|
||||
|
||||
set_option maxRecDepth 10000
|
||||
|
||||
def addALot (x: Nat) : StateM Nat Nat := do
|
||||
set x
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
modifyGet (λ y => ((), y + x))
|
||||
let y <- get
|
||||
pure y
|
||||
|
||||
#eval StateT.run' (addALot 2) 0
|
||||
|
|
@ -362,3 +362,9 @@
|
|||
run_config:
|
||||
<<: *time
|
||||
cmd: lean bv_decide_inequality.lean
|
||||
- attributes:
|
||||
description: big_do
|
||||
tags: [fast]
|
||||
run_config:
|
||||
<<: *time
|
||||
cmd: lean big_do.lean
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue