Skip to main content

axiom_usize_bitslice_index_model

vstd_extra::external

Function axiom_usize_bitslice_index_model 

Source 
pub broadcast proof fn axiom_usize_bitslice_index_model<T: BitStore, O: BitOrder>()
Expand description
requires
obeys_bitvec_model::<T, O>(),
ensures
#[trigger] obeys_bitslice_index_model::<T, O, usize>(),