fact: Fixpoint ByteBuffer_fold_left_pair {B} (f: Core.char -> Core.char -> B -> B) {sz: nat} n (v: ByteBuffer.t sz) (acc: B) (pad: Core.char) : B := match n, v with | 0%nat, _ => acc | _, @Vector.nil _ => acc | 1%nat, @Vector.cons _ x _ _ => f x pad acc | _, @Vector.cons _ x _ (@Vector.nil _) => f x pad acc | S (S n'), @Vector.cons _ x _ (@Vector.cons _ y _ tl) => ByteBuffer_fold_left_pair f n' tl (f x y acc) pad end.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString Permutation