
  0 | module Data.Maybe.Any
  1 | 
  2 | import Data.DPair
  3 | 
  4 | public export
  5 | data Any : (a -> Type) -> Maybe a -> Type where
  6 |   Here : {0 a : Type} -> {0 v : a} -> {0 p : a -> Type} -> p v -> Any p (Just v)
  7 | 
  8 | public export
  9 | Uninhabited (Any p Nothing) where
 10 |   uninhabited _ impossible
 11 | 
 12 | public export
 13 | extract : Any p (Just x) -> p x
 14 | extract (Here y) = y
 15 | 
 16 | public export
 17 | extractErased : {0 x : Maybe a} -> Any p x -> Exists p
 18 | extractErased (Here y) = Evidence _ y
 19 | 
 20 | public export
 21 | extractValue : {x : Maybe a} -> Any p x -> (v : a ** p v)
 22 | extractValue {x = Just v} (Here y) = (v ** y)
 23 | 
 24 | export
 25 | app : {0 a, b : Type} -> {0 x : a} -> {0 p : a -> Type} -> {0 y : b} -> {0 q : b -> Type} ->
 26 |       (p x -> q y) -> Any p (Just x) -> Any q (Just y)
 27 | app f = Here . f . extract
 28 | 
 29 | public export
 30 | mapProperty : (forall x. p x -> q x) -> Any p xs -> Any q xs
 31 | mapProperty f (Here x) = Here (f x)
 32 | 
 33 |