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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2024-06-19 10:57:58 -07:00 • committed by Leonardo de Moura
parent e8f768f9fd
commit de269060d1
2 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/compiler/phashmap.lean
View file

@ -62,9 +62,7 @@ IO.println m.stats;
check2 n 0 m;
let m := delLess 4900 m;
check2 n 4900 m;
IO.println m.size;
IO.println m.stats;
let m := delLess 4990 m;
check2 n 4990 m;
IO.println m.size;
IO.println m.stats

2
tests/compiler/phashmap.lean.expected.out
View file

@ -1,6 +1,4 @@
{ nodes := 1057, null := 27768, collisions := 0, depth := 3}
{ nodes := 529, null := 13900, collisions := 0, depth := 3}
50
{ nodes := 17, null := 478, collisions := 0, depth := 2}
5
{ nodes := 1, null := 27, collisions := 0, depth := 1}