Expand description
Unsigned big-endian base-256 format. Minimal big-endian base-256 integer conversion and formats.
Functionsยง
- lemma_
from_ be_ bytes_ lower_ bound - lemma_
from_ be_ bytes_ prepend - lemma_
from_ be_ bytes_ push - lemma_
from_ be_ bytes_ singleton - lemma_
from_ be_ bytes_ upper_ bound - lemma_
from_ to_ be_ bytes_ roundtrip - lemma_
nat_ from_ be_ bytes_ fits_ usize - lemma_
pow256_ succ - lemma_
to_ be_ bytes_ len_ bound - lemma_
to_ be_ bytes_ props - lemma_
to_ from_ be_ bytes_ roundtrip - lemma_
usize_ to_ be_ bytes_ len_ bound - nat_
from_ be_ bytes - nat_
to_ be_ bytes - size_
of_ usize - u64_
from_ be_ bytes - u64_
to_ be_ bytes - u64_
to_ be_ bytes_ first - u64_
to_ be_ bytes_ len - usize_
from_ be_ bytes_ exec - usize_
to_ be_ bytes_ exec - usize_
to_ be_ bytes_ in_ place - usize_
to_ be_ bytes_ len