fact: Definition WeatherSpec : ADT _ := Eval simpl in Def ADT { rep := QueryStructure WeatherSchema, Def Constructor0 Init : rep := empty,, Def Method1 AddCell (r : rep) (cell : WeatherSchema#CELLS) : rep * bool := Insert cell into r!CELLS, Def Method1 AddMeasurement (r : rep) (measurement : WeatherSchema#MEASUREMENTS) : rep * bool := Insert measurement into r!MEASUREMENTS, Def Method1 CountCells (r : rep) (area : W) : rep * nat := cnt <- Count (For (cell in r!CELLS) Where (area = cell!AREA_CODE) Return 1); ret (r, cnt), Def Method2 LocalMax (r : rep) (areaC : W) (measType : MeasurementType) : rep * (option W) := max <- MaxW (For (cell in r!CELLS) (measurement in r!MEASUREMENTS) Where (cell!AREA_CODE = areaC) Where (measurement!MEASUREMENT_TYPE = measType) Where (cell!CELL_ID = measurement!CELL_ID) Return measurement!VALUE); ret (r, max) }%methDefParsing.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory