Libraries.Data.List01.Quantifiers

Definitions

data All : (0 _ : (a -> Type)) -> List01 ne 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:

Nil : All p []

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

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

  Push in the property from the list level with element level

Totality: total
Visibility: public export

pullOut : List01 ne (Subset a p) -> Subset (List01 ne a) (All p)

  Pull the elementwise property out to the list level

Totality: total
Visibility: public export