Skip to main content

axiom_usize_bitvec_model

vstd_extra::external

Function axiom_usize_bitvec_model 

Source 
pub broadcast proof fn axiom_usize_bitvec_model()
Expand description
ensures
#[trigger] obeys_bitvec_model::<usize, Lsb0>(),