pub unsafe fn lean_string_utf8_get_fast(
    s: b_lean_obj_arg,
    i: b_lean_obj_arg
) -> u32