[m-rev.] for review: Clarify behaviour of upper bounds functions for array types.

[Julien Fischer]

Hi Peter,

On Wed, 29 Nov 2017, Peter Wang wrote:

> Would making 'max' semi-deterministic have been a better choice,

At the time it was added, yes.

> or just annoying in practice?

We probably would have added det_max alongside it in any case.

> Anyway, it is what we have.

> It might be viable still to make array.least_index and array.greatest_index
> fail for empty arrays. The names suggest to me that they should always
> return valid indices on success, more so than min/max.

I would add, det_least_index and semidet_least_index which throw an
exception and fail for an empty array respectively.  The existing
least_index should be deprecated and after a while semidet_least_index
should become least_index.

Ditto for gratest_index.

The diff is fine.

Julien.