#include "share/atspre_staload.hats"

staload "kernel/writer.sats"
dynload "kernel/writer.dats"

fn string_length {n:nat} (str: string (n)) : size_t (n) = let
  fun loop {i:nat | i <= n} .<n-i>. (str: string n, i: size_t i): size_t (n) =
    if string_isnot_atend (str, i) then loop (str, succ(i)) else i
in
  loop (str, i2sz(0))
end

implement main0 () = print_char('X')