Added docs for anyElim
commitace102003bbeb3d7eda1d11b30406003155068c6
authorDaniel Waterworth <da.waterworth@gmail.com>
dateThu 29 Oct 2015, 12:09 (11 years ago)
parent98f1bec
libs/base/Data/Vect/Quantifiers.idr+1
@@ -19,6 +19,7 @@ anyNilAbsurd (There _) impossible
1919instance Uninhabited (Any p Nil) where
2020 uninhabited = anyNilAbsurd
2121
22+||| Eliminator for `Any`
2223anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
2324anyElim _ f (Here p) = f p
2425anyElim f _ (There p) = f p
libs/contrib/Data/List/Quantifiers.idr+1
@@ -19,6 +19,7 @@ anyNilAbsurd (There _) impossible
1919instance Uninhabited (Any p Nil) where
2020 uninhabited = anyNilAbsurd
2121
22+||| Eliminator for `Any`
2223anyElim : {xs : List a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
2324anyElim _ f (Here p) = f p
2425anyElim f _ (There p) = f p