Skip to main content

extern_spec_T_A_Vec_T_A_remove

creusot_std::std::vec

Function extern_spec_T_A_Vec_T_A_remove 

Source 
pub fn extern_spec_T_A_Vec_T_A_remove<T, A: Allocator>(
    self_: &mut Vec<T, A>,
    ix: usize,
) -> T
Expand description

extern spec for Vec<T, A>::remove

This is not a real function: its only use is for documentation.

ghost

requires 

self

ensures 

self

ensures 

self

ensures 

self