Skip to main content

lemma_i8_value_roundtrip

vest_lib::combinators::sints::spec

Function lemma_i8_value_roundtrip 

Source 
pub broadcast proof fn lemma_i8_value_roundtrip(o: i8)
Expand description
ensures
#[trigger] ((o as u8) as i8) == o,