Expand description
Unsigned big-endian base-128 (VLQ) format. Big-endian base-128 integer encoding and in-place conversion helpers.
Structs§
Constants§
Functions§
- base128_
fmt - lemma_
base128_ fmt_ byte_ len - lemma_
base128_ fmt_ sound_ nonmal_ inv - lemma_
base128_ fmt_ unambiguous - lemma_
from_ base128_ push - lemma_
from_ base128_ upper_ bound - lemma_
from_ to_ base128_ roundtrip - lemma_
nat_ from_ base128_ bounds - lemma_
pow128_ succ - lemma_
to_ base128_ len_ bound - lemma_
to_ base128_ len_ bounds - lemma_
to_ base128_ props - lemma_
to_ from_ base128_ roundtrip - nat_
from_ base128 - nat_
to_ base128 - uint_
from_ base128 - uint_
to_ base128 - uint_
to_ base128_ in_ place - uint_
to_ base128_ len