flat_map_singleton

creusot_contracts::logic::seq

Function flat_map_singleton 

Source 
pub fn flat_map_singleton<A, B>()
Expand description

(open) 

{}

ensures

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