extern
fun strlen {m,n:nat} (buf: &strbuf (m, n)):<> size_t n
implement strlen {m,n} (buf) = loop (buf, 0) where {
fun loop {i:nat | i <= n} .<n-i>.
(buf: &strbuf (m, n), i: size_t i):<> size_t n =
if strbuf_is_atend (buf, i) then i else loop (buf, i+1)
}
implement
main (argc, argv) = let
val () = assertloc (argc >= 2)
val str = string1_of_string (argv.[1])
val len = strlen (!p_buf) where {
val (vbox pf_buf | p_buf) = strbuf_of_string1 str
} in
print "str = "; print str; print " and len = "; print len; print_newline ()
end