@@ -5,9 +5,12 @@ data Any : (P : a -> Type) -> Vect n a -> Type where
55 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
66
77anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8−anyNilAbsurd (Here _) impossible
8+anyNilAbsurd (Here _) impossible
99anyNilAbsurd (There _) impossible
1010
11+instance Uninhabited (Any p Nil) where
12+ uninhabited = anyNilAbsurd
13+
1114anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
1215anyElim _ f (Here p) = f p
1316anyElim f _ (There p) = f p