fact: Fixpoint align_format_list {A} (A_format_align : A -> CacheFormat -> {n : _ & ByteBuffer.t n} * CacheFormat) (As : list A) (ce : CacheFormat) : {n : _ & ByteBuffer.t n} * CacheFormat := match As with | nil => (existT _ _ (Vector.nil _), ce) | a :: As' => let (b, ce') := A_format_align a ce in let (b', ce'') := align_format_list A_format_align As' ce' in (existT _ _ (append (projT2 b) (projT2 b')), ce'') end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BaseFormats Bedrock.Word