
  0 | module Libraries.Data.List.Quantifiers.Extra
  1 | 
  2 | import Data.List
  3 | import Data.List.Quantifiers
  4 | import Decidable.Equality
  5 | 
  6 | %default total
  7 | 
  8 | export
  9 | lookup : {xs : List a} -> DecEq a => (v : a) -> All p xs -> Maybe (p v)
 10 | lookup v [] = Nothing
 11 | lookup v (px :: pxs)
 12 |   = case decEq (head xs) v of
 13 |       No _ => lookup v pxs
 14 |       Yes Refl => Just px
 15 |