git.iko.soy/Idris-dev
on master help sign in
Added docs for anyElim
ace1020Daniel Waterworth
libs/base/Data/Vect/Quantifiers.idr+1
compare with master
unifiedsplit
@@ -19,6 +19,7 @@ anyNilAbsurd (There _) impossible
19instance Uninhabited (Any p Nil) where
19instance Uninhabited (Any p Nil) where
20 uninhabited = anyNilAbsurd
20 uninhabited = anyNilAbsurd
21
21
22+||| Eliminator for `Any`
22anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
23anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
23anyElim _ f (Here p) = f p
24anyElim _ f (Here p) = f p
24anyElim f _ (There p) = f p
25anyElim f _ (There p) = f p
libs/contrib/Data/List/Quantifiers.idr+1
@@ -19,6 +19,7 @@ anyNilAbsurd (There _) impossible
19instance Uninhabited (Any p Nil) where
19instance Uninhabited (Any p Nil) where
20 uninhabited = anyNilAbsurd
20 uninhabited = anyNilAbsurd
21
21
22+||| Eliminator for `Any`
22anyElim : {xs : List a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
23anyElim : {xs : List a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
23anyElim _ f (Here p) = f p
24anyElim _ f (Here p) = f p
24anyElim f _ (There p) = f p
25anyElim f _ (There p) = f p