diff options
| author | Emilio Jesus Gallego Arias | 2018-10-17 23:03:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-18 19:35:57 +0200 |
| commit | 8303c9cab6bc403dfc209f65287b67e883a35711 (patch) | |
| tree | 9e6a086583aec8c58ab43c489cc3b863f500a48f /dev/base_include | |
| parent | c3823156da73a63967d9d472e21560af1585b271 (diff) | |
[clib] Provide `filter_range` function.
This is very useful to compute efficiently a list of prefixes. Will be
used in conjunction with the nametab to provide completion.
Example of use:
```
let cprefix x y = String.(compare x (sub y 0 (min (length x) (length y)))) in
M.filter_range (cprefix "foo") m
```
We could of course maintain a trie, but this is less invasive an
should work at our scale.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions
