Skip to content

Instantly share code, notes, and snippets.

@ctford
Created February 12, 2017 16:50
Show Gist options
  • Save ctford/0eccc8af971becf4fb0a3be6aa86cd42 to your computer and use it in GitHub Desktop.
Save ctford/0eccc8af971becf4fb0a3be6aa86cd42 to your computer and use it in GitHub Desktop.
A function that uses a membership proof to safely locate a tuple in a list.
locate : Eq a => (key : a) -> (entries : List (a, b)) -> {auto membership : Elem key (map Prelude.Basics.fst entries)} -> b
locate {membership} _ [] = absurd membership
locate {membership = Here} key ((key, value) :: _) = value
locate {membership = (There later)} key (_ :: entries) = locate key entries {membership = later}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment