-- Strings as arrays of characters. Any Nat index is accepted, and an
-- out-of-range index is caught only when the program runs.

def s2ac (s : String) : Array Char := s.toList.toArray

def hello : Array Char := s2ac "hello"

def get (s : Array Char) (i : Nat) : Except String Char :=
  match s[i]? with
  | some c => .ok c
  | none   => .error "index out of range"

-- Except.ok 'e'
#eval get hello 1
-- Except.error "index out of range"
#eval get hello 5
-- error: Nat has no negative numbers
-- #eval get hello (-1)