fact: Fixpoint FlagsSigs {n'} (subtopics : Vector.t (Fin.t n) n') : Vector.t methSig (n' * 2) := match subtopics in Vector.t _ n' return Vector.t methSig (n' * 2) with | Vector.nil => Vector.nil _ | Vector.cons topic _ topics' => Vector.cons _ (GetFlagSig topic) _ (Vector.cons _ (SetFlagSig topic) _ (FlagsSigs topics')) end.
imports: Coq.Strings.String Coq.Bool.Bool Coq.Lists.List Coq.Arith.Arith Coq.Program.Program Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTNotation Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements Fiat.Fiat4Monitors.RADL_Topics Fiat.Fiat4Monitors.RADL_Flag Bedrock.Memory