Function vstd::slice::axiom_slice_get_usize
source · pub broadcast proof fn axiom_slice_get_usize<T>(v: &[T], i: usize)Expand description
ensures
i < v.len() ==> (#[trigger] spec_slice_get(v, i) === Some(&v[i as int])),i >= v.len() ==> spec_slice_get(v, i).is_none(),