seq_tracked_empty

vstd_extra::seq_extra

Function seq_tracked_empty 

Source 
pub proof fn seq_tracked_empty<T>() -> tracked res : Seq<T>
Expand description
ensures
res == Seq::<T>::empty(),