
  0 | module Data.Maybe.All
  1 | 
  2 | public export
  3 | data All : (a -> Type) -> Maybe a -> Type where
  4 |   Nil : All p Nothing
  5 |   Value : {0 x : a} -> p x -> All p (Just x)
  6 | 
  7 | export
  8 | (.value) : {0 a : Type} -> {0 p : a -> Type} -> {0 x : a} -> All p (Just x) -> p x
  9 | (.value) (Value y) = y
 10 | 
 11 | export
 12 | app : {0 a, b : Type} -> {0 x : a} -> {0 p : a -> Type} -> {0 y : b} -> {0 q : b -> Type} ->
 13 |       (p x -> q y) -> All p (Just x) -> All q (Just y)
 14 | app f = Value . f . (.value)
 15 | 
 16 | export
 17 | fromMaybe : {0 a : Type} -> {0 p : a -> Type} ->
 18 |             ((x : a) -> p x) -> (m : Maybe a) -> All p m
 19 | fromMaybe f Nothing = []
 20 | fromMaybe f (Just x) = Value (f x)
 21 | 
 22 | public export
 23 | mapProperty : (forall x. p x -> q x) -> All p xs -> All q xs
 24 | mapProperty f [] = []
 25 | mapProperty f (Value x) = Value (f x)
 26 | 
 27 |