fact: Definition decode_unused_word' (s : nat) (b : T) : option (unit * T) := Ifopt monoid_dequeue_word s b as b' Then Some (tt, snd b') Else None.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats