Skip to main content

lemma_from_be_bytes_singleton

vest_lib::primitives::base256

Function lemma_from_be_bytes_singleton 

Source 
pub proof fn lemma_from_be_bytes_singleton(b: u8)
Expand description
ensures
nat_from_be_bytes(seq![b]) == b as nat,