pub unsafe fn lean_string_length(o: b_lean_obj_arg) -> lean_obj_res