fact: Definition decode_ascii (b : B) (cd : CacheDecode) : option (ascii * B * CacheDecode) := `(n, b, cd) <- decode_word (sz:=8) b cd; Some (ascii_of_N (wordToN n), b, cd).
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Numbers.BinNums Coq.NArith.BinNat