Idris2Doc : Data.CheckedEmpty.List.Properties.Quantifiers

Data.CheckedEmpty.List.Properties.Quantifiers

(source)
Definitions
allMapForall : ((0 _ : Elem x xs) -> p (f x)) -> All p (map f xs)
  Totality: total
  Visibility: export
allElem : ((0 _ : Elem x xs) -> p x) -> All p xs
  Totality: total
  Visibility: export
allTrue : p x -> All p xs
  Totality: total
  Visibility: export
allMap : All (p . f) xs -> All p (map f xs)
  Totality: total
  Visibility: export