Re-exports§
pub use super::view::View;
Structs§
Traits§
Functions§
- _verus_
external_ ⚠fn_ specification_ 14_ str_ 32__ 58__ 58__ 32_ is__ ascii - _verus_
external_ ⚠fn_ specification_ 15_ str_ 32__ 58__ 58__ 32_ to__ owned - _verus_
external_ ⚠fn_ specification_ 16_ str_ 32__ 58__ 58__ 32_ as__ bytes - _verus_
external_ ⚠fn_ specification_ 17_ str_ 32__ 58__ 58__ 32_ len - _verus_
external_ ⚠fn_ specification_ 18_ str_ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 19_ str_ 32__ 58__ 58__ 32_ is__ char__ boundary - _verus_
external_ ⚠fn_ specification_ 20_ str_ 32__ 58__ 58__ 32_ split__ at - _verus_
external_ ⚠fn_ specification_ 21_ str_ 32__ 58__ 58__ 32_ from__ utf8__ unchecked - _verus_
external_ ⚠fn_ specification_ 22__ 60__ 32_ T_ 32_ as_ 32_ ToString_ 32__ 62__ 32__ 58__ 58__ 32_ to__ string - _verus_
external_ ⚠fn_ specification_ 23_ String_ 32__ 58__ 58__ 32_ as__ str - _verus_
external_ ⚠fn_ specification_ 24__ 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_ 25__ 60__ 32_ String_ 32_ as_ 32_ Clone_ 32__ 62__ 32__ 58__ 58__ 32_ clone - _verus_
external_ ⚠fn_ specification_ 26__ 60__ 32_ String_ 32_ as_ 32_ Partial Eq_ 32__ 62__ 32__ 58__ 58__ 32_ eq - _verus_
external_ ⚠fn_ specification_ 27_ String_ 32__ 58__ 58__ 32_ new - _verus_
external_ ⚠fn_ specification_ 28_ String_ 32__ 58__ 58__ 32_ push - _verus_
external_ ⚠fn_ specification_ 29_ String_ 32__ 58__ 58__ 32_ pop - _verus_
external_ ⚠fn_ specification_ 30_ String_ 32__ 58__ 58__ 32_ push__ str - _verus_
external_ ⚠fn_ specification_ 31_ String_ 32__ 58__ 58__ 32_ is__ empty - _verus_
external_ ⚠fn_ specification_ 32_ String_ 32__ 58__ 58__ 32_ clear - _verus_
external_ ⚠fn_ specification_ 33__ 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_ 34_ str_ 32__ 58__ 58__ 32_ chars - _verus_
external_ ⚠fn_ specification_ 35__ 60__ 32__ 40_ Bound_ 32__ 60__ 32_ usize_ 32__ 62__ 32__ 44__ 32_ Bound_ 32__ 60__ 32_ usize_ 32__ 62__ 41__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 36__ 60__ 32__ 40_ Bound_ 32__ 60__ 32_ usize_ 32__ 62__ 32__ 44__ 32_ Bound_ 32__ 60__ 32_ usize_ 32__ 62__ 41__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 37__ 60__ 32__ 40_ Bound_ 32__ 60__ 32_ usize_ 32__ 62__ 32__ 44__ 32_ Bound_ 32__ 60__ 32_ usize_ 32__ 62__ 41__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 38__ 60__ 32__ 40_ Bound_ 32__ 60__ 32_ usize_ 32__ 62__ 32__ 44__ 32_ Bound_ 32__ 60__ 32_ usize_ 32__ 62__ 41__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 39__ 60__ 32_ Range_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 40__ 60__ 32_ Range_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 41__ 60__ 32_ Range_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 42__ 60__ 32_ Range_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 43__ 60__ 32_ Range From_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 44__ 60__ 32_ Range From_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 45__ 60__ 32_ Range From_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 46__ 60__ 32_ Range From_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 47__ 60__ 32_ Range Full_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 48__ 60__ 32_ Range Full_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 49__ 60__ 32_ Range Full_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 50__ 60__ 32_ Range Full_ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 51__ 60__ 32_ Range Inclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 52__ 60__ 32_ Range Inclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 53__ 60__ 32_ Range Inclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 54__ 60__ 32_ Range Inclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 55__ 60__ 32_ Range To_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 56__ 60__ 32_ Range To_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 57__ 60__ 32_ Range To_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 58__ 60__ 32_ Range To_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - _verus_
external_ ⚠fn_ specification_ 59__ 60__ 32_ Range ToInclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get - _verus_
external_ ⚠fn_ specification_ 60__ 60__ 32_ Range ToInclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index - _verus_
external_ ⚠fn_ specification_ 61__ 60__ 32_ Range ToInclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ get__ mut - _verus_
external_ ⚠fn_ specification_ 62__ 60__ 32_ Range ToInclusive_ 32__ 60__ 32_ usize_ 32__ 62__ 32_ as_ 32_ Slice Index_ 32__ 60__ 32_ str_ 32__ 62__ 32__ 62__ 32__ 58__ 58__ 32_ index__ mut - axiom_
new_ strlit_ view_ id - axiom_
str_ literal_ get_ char - axiom_
str_ literal_ len - group_
string_ axioms - into_
iter_ elts - is_
ascii - is_
ascii_ concat - is_
ascii_ spec_ bytes - str_
slice_ in_ bounds - str_
slice_ index_ mut_ postcondition - str_
slice_ index_ postcondition - string_
is_ ascii - strlit_
view_ id - to_
string_ from_ display_ ensures - to_
string_ from_ display_ ensures_ for_ str