data Any : (0 _ : (a -> Type)) -> Vect n a -> Type
A proof that some element of a vector satisfies some property
@ p the property to be satsified
Totality: total
Visibility: public export
Constructors:
Here : p x -> Any p (x :: xs)
A proof that the satisfying element is the first one in the `Vect`
There : Any p xs -> Any p (x :: xs)
A proof that the satsifying element is in the tail of the `Vect`
Hints:
Uninhabited (Any p [])
Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p (x :: xs))
anyElim : (Any p xs -> b) -> (p x -> b) -> Any p (x :: xs) -> b
Eliminator for `Any`
Totality: total
Visibility: public exportany : ((x : a) -> Dec (p x)) -> (xs : Vect n a) -> Dec (Any p xs)
Given a decision procedure for a property, determine if an element of a
vector satisfies it.
@ p the property to be satisfied
@ dec the decision procedure
@ xs the vector to examine
Totality: total
Visibility: public exportmapProperty : (p x -> q x) -> Any p l -> Any q l
- Totality: total
Visibility: export data All : (0 _ : (a -> Type)) -> Vect n a -> Type
A proof that all elements of a vector satisfy a property. It is a list of
proofs, corresponding element-wise to the `Vect`.
Totality: total
Visibility: public export
Constructors:
Nil : All p []
(::) : p x -> All p xs -> All p (x :: xs)
Hint: Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All p (x :: xs))
negAnyAll : Not (Any p xs) -> All (Not . p) xs
If there does not exist an element that satifies the property, then it is
the case that all elements do not satisfy.
Totality: total
Visibility: exportnotAllHere : Not (p x) -> Not (All p (x :: xs))
- Totality: total
Visibility: export notAllThere : Not (All p xs) -> Not (All p (x :: xs))
- Totality: total
Visibility: export all : ((x : a) -> Dec (p x)) -> (xs : Vect n a) -> Dec (All p xs)
Given a decision procedure for a property, decide whether all elements of
a vector satisfy it.
@ p the property
@ dec the decision procedure
@ xs the vector to examine
Totality: total
Visibility: public exportmapProperty : (p x -> q x) -> All p l -> All q l
- Totality: total
Visibility: export imapProperty : (0 i : (Type -> Type)) -> (i a => p a -> q a) -> All i types => All p types -> All q types
- Totality: total
Visibility: public export