Function extern_spec_T__slice_T_last_mut 

pub fn extern_spec_T__slice_T_last_mut<T>(self_: &mut [T]) -> Option<&mut T>

extern spec for slice<T>::last_mut

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

ghost

ensures

(result == None) == (self@.len() == 0)

ensures

self

ensures

forall<x> result == Some(x) ==> (^self)[self@.len() - 1] == ^x

ensures

(*self)@.len() == (^self)@.len()

ensures

forall<i> 0 <= i && i < (*self)@.len() - 1 ==> (*self)[i] == (^self)[i]