flat_map_push_back

creusot_contracts::logic::seq

Function flat_map_push_back 

Source 
pub fn flat_map_push_back<A, B>(xs: Seq<A>)
Expand description

(open)

if xs.len() > 0 {
    flat_map_push_back::<A, B>(xs.tail());
    proof_assert! { forall<x: A> xs.tail().push_back(x) == xs.push_back(x).tail() }
}

ensures

forall<x: A, f: Mapping<A, Seq<B>>> xs.push_back(x).flat_map(f) == xs.flat_map(f).concat(f.get(x))