fact: Definition decode_strict {S T} {cache : Cache} {monoid : Monoid T} (decode : DecodeM S T) : DecodeM (S * T) T := fun cd bs => Ifopt decode cd bs as abscd' Then Some (fst abscd', mempty, snd abscd') Else None.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache