Module string 

Re-exports

pub use super::view::View;

Structs

ExChars

ExString

Traits

StrSliceExecFns

StringExecFns

StringExecFnsIsAscii

StringSliceAdditionalSpecFns

Functions

_verus_external_fn_specification_15_str_32__58__58__32_is__ascii^⚠

_verus_external_fn_specification_16_str_32__58__58__32_to__owned^⚠

_verus_external_fn_specification_17_str_32__58__58__32_as__bytes^⚠

_verus_external_fn_specification_18_str_32__58__58__32_len^⚠

_verus_external_fn_specification_19_str_32__58__58__32_is__empty^⚠

_verus_external_fn_specification_20_str_32__58__58__32_is__char__boundary^⚠

_verus_external_fn_specification_21_str_32__58__58__32_split__at^⚠

_verus_external_fn_specification_22_str_32__58__58__32_from__utf8__unchecked^⚠

_verus_external_fn_specification_23__60__32_T_32_as_32_ToString_32__62__32__58__58__32_to__string^⚠

_verus_external_fn_specification_24_String_32__58__58__32_as__str^⚠

_verus_external_fn_specification_25__60__32_String_32_as_32_core_32__58__58__32_ops_32__58__58__32_Deref_32__62__32__58__58__32_deref^⚠

_verus_external_fn_specification_26__60__32_String_32_as_32_Clone_32__62__32__58__58__32_clone^⚠

_verus_external_fn_specification_27__60__32_String_32_as_32_PartialEq_32__62__32__58__58__32_eq^⚠

_verus_external_fn_specification_28_String_32__58__58__32_new^⚠

_verus_external_fn_specification_29__60__32_String_32_as_32_core_32__58__58__32_default_32__58__58__32_Default_32__62__32__58__58__32_default^⚠

_verus_external_fn_specification_30_str_32__58__58__32_chars^⚠

_verus_external_fn_specification_31_Chars_32__58__58__32__60__32__39_a_32__62__32__58__58__32_next^⚠

axiom_spec_iter

axiom_str_literal_get_char

axiom_str_literal_len

group_string_axioms

into_iter_elts

is_ascii

is_ascii_concat

is_ascii_spec_bytes

next_post

next_postcondition

spec_iter

string_is_ascii

to_string_from_display_ensures

to_string_from_display_ensures_for_str