fact: Definition format_option (format_Some : FormatM S T) (format_None : FormatM () T) : FormatM (option S) T := fun a_opt => If_Opt_Then_Else a_opt format_Some (format_None ()).
imports: Fiat.Common Fiat.Computation Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats