fact: Fixpoint format_list (xs : list A) (ce : CacheFormat) : Comp (T * CacheFormat) := match xs with | nil => ret (mempty, ce) | x :: xs' => `(b1, env1) <- format_A x ce; `(b2, env2) <- format_list xs' env1; ret (mappend b1 b2, env2) end%comp.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.Base.FixFormat Coq.Lists.List