
  0 | module Data.CheckedEmpty.List.Lazy.Properties.Map
  1 | 
  2 | import Data.Maybe
  3 | 
  4 | import Data.CheckedEmpty.List.Lazy
  5 | import Data.CheckedEmpty.List.Lazy.Elem
  6 | import Data.CheckedEmpty.List.Lazy.Quantifiers
  7 | 
  8 | %default total
  9 | 
 10 | export
 11 | mapId : (xs : LazyLst ne a) -> map Prelude.id xs === xs
 12 | mapId $ []            = Refl
 13 | mapId $ x :: Delay xs = cong (x ::) $ mapId xs
 14 | 
 15 | export
 16 | allMapMaybeJust : {f : a -> Maybe b} ->
 17 |                   {xs : LazyLst ne a} ->
 18 |                   ((x : a) -> (0 _ : IsJust $ f x) -> p $ fromJust (f x)) ->
 19 |                   All p $ mapMaybe f xs
 20 | allMapMaybeJust {xs=[]}      h = []
 21 | allMapMaybeJust {xs=x :: xs} h with (f x) proof 0 prf
 22 |   _ | Nothing = allMapMaybeJust h
 23 |   _ | Just y  = do
 24 |     let yIsJust : IsJust (f x) = rewrite prf in ItIsJust
 25 |     let Refl : y === fromJust (f x) = rewrite prf in Refl
 26 |     h x yIsJust :: allMapMaybeJust h
 27 |