Skip to content

Instantly share code, notes, and snippets.

@edwinb

edwinb/nestedrec.idr

Last active August 29, 2015 14:00
Show Gist options
  • Save edwinb/14e91a2c71628d5cac9d to your computer and use it in GitHub Desktop.
Save edwinb/14e91a2c71628d5cac9d to your computer and use it in GitHub Desktop.
Download ZIP
Nested record update syntax
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment