Skip to main content

bitvec_index_value

vstd_extra::external

Function bitvec_index_value 

Source 
pub uninterp spec fn bitvec_index_value<'a, T: BitStore, O: BitOrder, Idx>(
    bv: &'a BitVec<T, O>,
    idx: Idx,
) -> &'a <BitVec<T, O> as Index<Idx>>::Output
where
    BitSlice<T, O>: Index<Idx>,
Expand description

Reads a single bit (panics if idx is out of bounds); the usize result is related to the model by axiom_bitvec_index_usize.