docs: public static /*@pure@*/ int minIndex(int[] ints) {
  
      int minimum = 0;
      int minIndex = 0;
  
      for (int i = 0; i < ints.length; i++) {
        if ((i == 0) || (ints[i] < minimum)) {
  	minIndex = i;
  	minimum = ints[i];
        }
      }
  
      return minIndex;
    }