
  0 | 
  1 | module Data.CheckedEmpty.List.Properties.Quantifiers
  2 | 
  3 | import Data.CheckedEmpty.List
  4 | import Data.CheckedEmpty.List.Elem
  5 | import Data.CheckedEmpty.List.Properties.Map
  6 | import Data.CheckedEmpty.List.Quantifiers
  7 | 
  8 | %default total
  9 | 
 10 | export
 11 | allMapForall : {0 f : a -> b} -> {xs : Lst ne a} ->
 12 |                ({x : a} -> (0 _ : Elem x xs) -> p (f x)) ->
 13 |                All p $ map f xs
 14 | allMapForall {xs=[]}      _ = []
 15 | allMapForall {xs=x :: xs} h = h Here :: allMapForall (\e => h $ There e)
 16 | 
 17 | export
 18 | allElem : {xs : Lst ne a} -> ({x : a} -> (0 _ : Elem x xs) -> p x) -> All p xs
 19 | allElem h = rewrite sym $ mapId {xs} in allMapForall h
 20 | 
 21 | export
 22 | allTrue : {xs : Lst ne a} -> ({x : a} -> p x) -> All p xs
 23 | allTrue h = allElem $ \_ => h
 24 | 
 25 | export
 26 | allMap : {0 xs : Lst ne a} -> {0 f : a -> b} ->
 27 |          All (p . f) xs -> All p $ map f xs
 28 | allMap $ []      = []
 29 | allMap $ h :: hs = h :: allMap hs
 30 |