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