diff options
| author | Pierre-Marie Pédrot | 2020-08-20 17:28:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-21 16:47:20 +0200 |
| commit | 72500ec169237ca98a5cfd5e4c0ff92b9c555eee (patch) | |
| tree | f807aa924236a192bd80633d5720347194cd77da /interp | |
| parent | 3d430a47d91bc541dcd6576063471c44fc457bf9 (diff) | |
Use a map function instead of a fold when freezing summaries.
This is O(n) instead of O(n log n) and should be more efficient in practice.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions