- notAllThere : Not (All P
xs) ->
All P
(x ::
xs) ->
Void
- notAllHere : Not (P x) ->
All P
(x ::
xs) ->
Void
- negAnyAll : Not (Any P
xs) ->
All (\x =>
Not (P x))
xs
If there does not exist an element that satifies the property, then it is
the case that all elements do not satisfy.
- anyNilAbsurd : Any P
[] ->
Void
No element of an empty vector satisfies any property
- anyElim : (Any P
xs ->
b) ->
(P x ->
b) ->
Any P
(x ::
xs) ->
b
Eliminator for Any
- any : (dec : (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
- all : (dec : (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
- data Any : (P : a ->
Type) ->
Vect n
a ->
Type
A proof that some element of a vector satisfies some property
- P
the property to be satsified
- 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
- data All : (P : 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
.
- Nil : All P
[]
- (::) : P x ->
All P
xs ->
All P
(x ::
xs)
- Fixity
- Left associative, precedence 7