Skip to main content

is_first_zero

vstd_extra::seq_extra

Function is_first_zero 

Source 
pub open spec fn is_first_zero(s: Seq<bool>, i: int) -> bool
Expand description
{
    &&& 0 <= i <= s.len()
    &&& (forall |j: int| 0 <= j < i ==> s[j])
    &&& (i < s.len() ==> !s[i])

}

The index of the first false bit in s, or s.len() if every bit is true.