Module spec 

Specification trait implementations for this combinator. Specifications for fixed- and variable-length bytes.

Functions

array_from_seq

axiom_array_from_seq

lemma_array_from_seq_roundtrip

lemma_tail_and_then_consistent

tail_and_then_lemmas