Skip to main content

lemma_u8_and_zero

vstd_extra::bits

Function lemma_u8_and_zero 

Source 
pub proof fn lemma_u8_and_zero(x: u8)
Expand description
ensures
0u8 & x == 0u8,

AND-ing the zero word with any word is zero.