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:

All (Eq . p) xs => Eq (Any p xs)

All (Show . p) xs => Show (Any p xs)

All (Uninhabited . p) xs => Uninhabited (Any p xs)

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 (Ord . p) xs => All (Eq . p) xs

All (Monoid . p) xs => All (Semigroup . p) xs

All (Eq . p) xs => Eq (Any p xs)

All (Eq . p) xs => Eq (All p xs)

All (Monoid . p) xs => Monoid (All p xs)

All (Ord . p) xs => Ord (All p xs)

All (Semigroup . p) xs => Semigroup (All p xs)

All (Show . p) xs => Show (Any p xs)

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

All (Uninhabited . p) xs => Uninhabited (Any p xs)

Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All 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

toDPair : Any p xs -> DPair a p

  Forget the membership proof

Totality: total
Visibility: public export

toExists : Any p xs -> Exists p

  Forget the membership proof

Totality: total
Visibility: export

anyToFin : Any p xs -> Fin (length xs)

Totality: total
Visibility: public export

pushOut : Functor p => Any (p . q) xs -> p (Any q xs)

Totality: total
Visibility: public export

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

HSnocList : SnocList Type -> Type

  A heterogeneous snoc-list of arbitrary types

Totality: total
Visibility: public export

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

  Push in the property from the list level with element level

Totality: total
Visibility: public export

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

  Pull the elementwise property out to the list level

Totality: total
Visibility: public export

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

Totality: total
Visibility: export

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

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

pushOut : Applicative p => All (p . q) xs -> p (All q xs)

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

allAnies : All p xs -> SnocList (Any p xs)

Totality: total
Visibility: public export

altAll : Alternative p => All (p . q) xs -> p (Any q xs)

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