Data.List1.Quantifiers

Definitions

data Any : (0 _ : (a -> Type)) -> List1 a -> Type

  A proof that some element of a list satisfies some property
  
  @ p the property to be satisfied

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 `List1`

There : Any p xs -> Any p (x ::: xs)

  A proof that the satisfying element is in the tail of the `List1`

mapProperty : (p x -> q x) -> Any p l -> Any q l

  Modify the property given a pointwise function

Totality: total
Visibility: export

any : ((x : a) -> Dec (p x)) -> (xs : List1 a) -> Dec (Any p xs)

  Given a decision procedure for a property, determine if an element of a
  list satisfies it.
  
  @ p the property to be satisfied
  @ dec the decision procedure
  @ xs the list to examine

Totality: total
Visibility: public export

toExists : Any p xs -> Exists p

  Forget the membership proof

Totality: total
Visibility: export

data All : (0 _ : (a -> Type)) -> List1 a -> Type

  A proof that all elements of a list satisfy a property. It is a list of
  proofs, corresponding element-wise to the `List1`.

Totality: total
Visibility: public export
Constructor: 

(:::) : p x -> All p xs -> All p (x ::: xs)

Hint: 

Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All p (x ::: xs))

mapProperty : (p x -> q x) -> All p l -> All q l

  Modify the property given a pointwise function

Totality: total
Visibility: export

imapProperty : (0 i : (Type -> Type)) -> (i a => p a -> q a) -> All i types => All p types -> All q types

  Modify the property given a pointwise interface function

Totality: total
Visibility: public export

forget : All (const type) types -> List1 type

  Forget property source for a homogeneous collection of properties

Totality: total
Visibility: public export

all : ((x : a) -> Dec (p x)) -> (xs : List1 a) -> Dec (All p xs)

  Given a decision procedure for a property, decide whether all elements of
  a list satisfy it.
  
  @ p the property
  @ dec the decision procedure
  @ xs the list to examine

Totality: total
Visibility: public export

zipPropertyWith : (p x -> q x -> r x) -> All p xs -> All q xs -> All r xs

Totality: total
Visibility: export

HList1 : List1 Type -> Type

  A heterogeneous list of arbitrary types

Totality: total
Visibility: public export

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 it.

Totality: total
Visibility: export

anyNegAll : Any (Not . p) xs -> Not (All p xs)

  If there exists an element that doesn't satify the property, then it is
  not the case that all elements satisfy it.

Totality: total
Visibility: export

allNegAny : All (Not . p) xs -> Not (Any p xs)

  If none of the elements satisfy the property, then not any single one can.

Totality: total
Visibility: export

indexAll : Elem x xs -> All p xs -> p x

  Given a proof of membership for some element, extract the property proof for it

Totality: total
Visibility: public export

pushIn : (xs : List1 a) -> (0 _ : All p xs) -> List1 (Subset a p)

  Push in the property from the list level with element level

Totality: total
Visibility: public export

pullOut : List1 (Subset a p) -> Subset (List1 a) (All p)

  Pull the elementwise property out to the list level

Totality: total
Visibility: public export

pushInOutInverse : (xs : List1 a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf

Totality: total
Visibility: export

pushOutInInverse : (xs : List1 (Subset a p)) -> uncurry pushIn (pullOut xs) = xs

Totality: total
Visibility: export