Skip to main content

lemma_to_from_base128_roundtrip

vest_lib::primitives::base128

Function lemma_to_from_base128_roundtrip 

Source 
pub proof fn lemma_to_from_base128_roundtrip(n: nat)
Expand description
ensures
nat_from_base128(nat_to_base128(n)) == n,