@@ -5,9 +5,12 @@ data Any : (P : a -> Type) -> Vect n a -> Type where
5 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
5 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8−anyNilAbsurd (Here _) impossible
8+anyNilAbsurd (Here _) impossible
9anyNilAbsurd (There _) impossible
9anyNilAbsurd (There _) impossible
11+instance Uninhabited (Any p Nil) where
12+ uninhabited = anyNilAbsurd
11anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
14anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
12anyElim _ f (Here p) = f p
15anyElim _ f (Here p) = f p
13anyElim f _ (There p) = f p
16anyElim f _ (There p) = f p