fact: Definition SetFlagDef {n'} (subtopics : Vector.t (Fin.t n) n') (topic : Fin.t n') : cMethDef (Rep := Flags subtopics) (SetFlagSig (Vector.nth subtopics topic)) := Def Method _ (msg : rep, val : RADL_Flag) : unit := (SetFlag msg topic val, tt).
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