Structs§
Traits§
- Double
Ended Iterator Spec - Double
Ended Iterator Spec Impl - ExDouble
Ended Iterator - ExExact
Size Iterator - ExFrom
Iterator - ExInto
Iterator - ExIter
Step - ExIterator
- Exact
Size Iterator Spec - Exact
Size Iterator Spec Impl - From
Iterator Spec - From
Iterator Spec Impl - Iterator
Spec - Iterator
Spec Impl - Step
Spec - Step
Spec Impl
Functions§
- _verus_
external_ ⚠fn_ specification_ 433__ 60__ 32_ I_ 32_ as_ 32_ Into Iterator_ 32__ 62__ 32__ 58__ 58__ 32_ into__ iter - axiom_
from_ iterator_ ensures - filter_
fun - filter_
iter - filter_
keep - filter_
post - filter_
postcondition - group_
iter_ axioms - into_
iter_ remaining - iter_
into_ iter_ spec - map_fun
- map_
iter - map_
post - map_
postcondition - rev_
iter - rev_
post - rev_
postcondition - skip_
init_ n - skip_
iter - skip_
post - skip_
postcondition - take_
count - take_
iter - take_
post - take_
postcondition - trigger_
peek_ implications - zip_
iter_ fst - zip_
iter_ snd - zip_
post - zip_
postcondition