The more basic API, still named search_sorted, returns a Post n. The idea is that the elements of xs are fence sections, and we find the position between them (inclusive on either end) where x falls in the ordering.
In terms of this, we now define search_sorted_exact (better name?), which returns a Maybe n, which is the index of an element of xs that equals x exactly, or Nothing if such does not exist.
Also reorder the prelude slightly to try to both maintain semantic groupings and respect name resolution dependencies.
Context: https://github.com/google-research/dex-lang/pull/1296#issuecomment-1557554550
The more basic API, still named
search_sorted, returns aPost n. The idea is that the elements ofxsare fence sections, and we find the position between them (inclusive on either end) wherexfalls in the ordering.In terms of this, we now define
search_sorted_exact(better name?), which returns aMaybe n, which is the index of an element ofxsthat equalsxexactly, orNothingif such does not exist.Also reorder the prelude slightly to try to both maintain semantic groupings and respect name resolution dependencies.