(* Try 1, based on Hongwei's string_length
 * It did look simpler at one point, but attempting to debug
 * resulted in the following, which didn't help. Time to start over! *)

fun string_caps
  {n:nat| n > 0}
  (str: string(n)): string n =
  let
    //val sstr = string_of_string1(str)
    val [n:int] str = string1_of_string (str)
    val n = string_length (str)
    val initi:sizeLt(n) = size1_of_int1(0)
    fun loop (str: string n, i: sizeLt(n)): string n =
      let
        val [n:int] str = string1_of_string (str)
      in
        if i < n then
          let
            val x = toCaps(str[i])
            val x = tostring(x)
            val x = string1_of_string(x)
            val x = string_of_string1(x)
            val ii = i+1
            val xs = loop (str, ii)
            val xs = string1_of_string(xs)
            val xs = string_of_string1(xs)
            val xxs = x + xs
            val xxs = string1_of_string(xxs)
            val _ = print(xxs)
            val _ = $showtype(x)
            val _ = $showtype(xs)
            val _ = $showtype(xxs)
          in
            xxs
          end
        else string1_of_string("")
        //else string_of_string1(" ") //CHANGE THIS TO ""
      end
  in
    loop (str, initi)
  end // end of [string_caps]