fact: Fixpoint encode_string (xs : string) (ce : CacheFormat) : B * CacheFormat := match xs with | EmptyString => (mempty, ce) | String x xs' => let (b1, env1) := encode_ascii x ce in let (b2, env2) := encode_string xs' env1 in (mappend b1 b2, env2) end.
imports: Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.AsciiOpt Bedrock.Word Coq.Strings.Ascii Coq.Strings.String