fact: Definition FriendFinderSpec : ADT _ := Def ADT { rep := QueryStructure FriendFinderSchema, Def Constructor0 "Init" : rep := empty,, Def Method1 "AddPerson" (r : rep) (person : FriendFinderSchema#PEOPLE) : rep * bool := Insert person into r!PEOPLE, Def Method1 "AddCity" (r : rep) (city : FriendFinderSchema#CITIES) : rep * bool := Insert city into r!CITIES, Def Method2 "PeopleAround" (r : rep) (name : string) (distance : nat) : rep * (list string) := res <- For (person_me in r!PEOPLE) (person in r!PEOPLE) (city_me in r!CITIES) (city in r!CITIES) Where (person_me!NAME = name) Where (city_me!CITY = person_me!CITY) Where (city_me!LATITUDE - distance <= city!LATITUDE <= city_me!LATITUDE + distance) Where (city_me!LONGITUDE - distance <= city!LONGITUDE <= city_me!LONGITUDE + distance) Where (person!CITY = city!CITY) Return person!NAME; ret (r, res), Def Method1 "PeopleInCity" (r : rep) (city : string) : rep * nat := res <- Count (For (person in r!PEOPLE) Where (person!CITY = city) Return ()); ret (r, res) }%methDefParsing.
imports: Fiat.QueryStructure.Automation.MasterPlan