Data.SnocList.Quantifiers

Definitions

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

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

Totality: total
Visibility: public export
Constructors:

Here : p x -> Any p (xs :< x)

  A proof that the rightmost element in the `SnocList` satisfies p

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

  A proof that there is an element the tail of the `SnocList` satisfying p

Hints:

Uninhabited (Any p [<])

Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p (xs :< x))

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

  Modify the property given a pointwise function

Totality: total
Visibility: public export

any : ((x : a) -> Dec (p x)) -> (xs : SnocList 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)) -> SnocList a -> Type

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

Totality: total
Visibility: public export
Constructors:

Lin : All p [<]

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

Hints:

All Show (map p xs) => Show (All p xs)

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

length : All p xs -> Nat

Totality: total
Visibility: public export

(++) : All p xs -> All p ys -> All p (xs ++ ys)

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

lengthUnfold : (pxs : All p xs) -> length pxs = length xs

Totality: total
Visibility: export

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

  Modify the property given a pointwise function

Totality: total
Visibility: public 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 -> SnocList type

  Forget property source for a homogeneous collection of properties

Totality: total
Visibility: public export

all : ((x : a) -> Dec (p x)) -> (xs : SnocList 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

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

decide : ((x : a) -> Either (p x) (q x)) -> (xs : SnocList a) -> Either (All p xs) (Any q xs)

  If any `a` either satisfies p or q then given a Snoclist of as,
  either all values satisfy p
  or at least one of them sastifies q

Totality: total
Visibility: public export