Nested record update syntax

nestedrec.idr

  record Person : Nat -> Type where
         MkPerson : (name : String) ->
                    (age : Nat) ->
                    Person age
  
  record Event : Type where
         MkEvent : (name : String) -> (organiser : Person a) -> Event
  
  record Meeting : Int -> Type where
         MkMeeting : (event : Event) ->
                     (organiser : Person a) ->
                     (year : Int) ->
                     Meeting year
  
  new_organiser : String -> List (Meeting x) -> List (Meeting x)
  new_organiser n = map (record { event->organiser->name = n })
  
  next_year : Meeting x -> Meeting (x+1)
  next_year m = record { organiser->age
                            = record { organiser->age } m + 1,
                         event->organiser->age
                            = record { event->organiser->age } m + 1,
                         year = _ } m