fact: Fixpoint CharList_dequeue {numBytes} (l : ByteBuffer.t (S numBytes)) : bool * (ByteBuffer.t numBytes) * word 7 := let (b, w') := word_dequeue (ByteBuffer.hd l) in match numBytes return ByteBuffer.t (S numBytes) -> _ with | S numBytes' => fun l => match CharList_dequeue (ByteBuffer.tl l) with | (b', l'', tail) => (b, ByteBuffer.cons (WS b' w') l'', tail) end | 0 => fun _ => (b, ByteBuffer.nil, w') end l.
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