16 lines
730 B
Text
16 lines
730 B
Text
=== lean4-0001: guardCycle List vs HashSet ===
|
|
N=100 : defective=0.206ms fixed=0.027ms speedup=7.7x
|
|
N=500 : defective=3.366ms fixed=0.086ms speedup=39.1x
|
|
N=1000 : defective=7.688ms fixed=0.292ms speedup=26.3x
|
|
N=2000 : defective=38.064ms fixed=1.101ms speedup=34.6x
|
|
|
|
=== lean4-0002: inductive type check std::find vs set ===
|
|
K=N=100 : defective=0.319ms fixed=0.002ms speedup=146.7x
|
|
K=N=500 : defective=2.772ms fixed=0.011ms speedup=259.5x
|
|
K=N=1000: defective=14.088ms fixed=0.021ms speedup=678.3x
|
|
|
|
=== lean4-0003: fresh name generation ===
|
|
N=100 : defective=0.105ms fixed=0.004ms speedup=29.7x
|
|
N=500 : defective=3.317ms fixed=0.016ms speedup=205.6x
|
|
N=1000 : defective=19.888ms fixed=0.095ms speedup=209.7x
|
|
|