fact: Fixpoint VectorByteToWord {numBytes} (v : t char numBytes) : word (8 * numBytes) := match numBytes return t char numBytes -> word (8 * numBytes) with | 0 => fun _ => WO | S numBytes' => fun v => eq_rect _ word (Core.append_word (VectorByteToWord (Vector.tl v)) (Vector.hd v)) (8 * S numBytes') (sym_eq (NPeano.Nat.mul_succ_r _ _)) end v.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer Coq.Strings.String Coq.Vectors.Vector Fiat.Narcissus.Formats.WordOpt