fact: Definition AsciiToByte (a: Ascii.ascii) : B := match a with | Ascii.Ascii x x0 x1 x2 x3 x4 x5 x6 => Word.WS x (Word.WS x0 (Word.WS x1 (Word.WS x2 (Word.WS x3 (Word.WS x4 (Word.WS x5 (Word.WS x6 Word.WO))))))) end.
imports: Coq.Program.Program Fiat.CertifiedExtraction.Core Fiat.CertifiedExtraction.FacadeWrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Bedrock.Arrays Bedrock.Platform.Facade.examples.QsADTs Bedrock.Word