Data.CheckedEmpty.List.Lazy.Properties.Quantifiers

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