Commit 2023-05-07 09:18 598f6c11

feat: library_search tries most specific lemmas first, and then those with shorter names first (#3725) It turns out that DiscrTree.getMatch returns more specific results later than less specific ones, and so we want to put a .reverse in, as library_search is more likely to be able to make use of the more specific lemmas. Additionally, within each "batch" of lemmas in the DiscrTree, we sort them so that those with shorter names are tried before those with longer names. You shouldn't expect this to be anymore successful, I think, but maybe the user will be happier getting shorter results rather than longer ones. See some further discussion at zulip.

• depends on: #3771