Data.Maybe.Any

Definitions

data Any : (a -> Type) -> Maybe a -> Type

Totality: total
Visibility: public export
Constructor: 

Here : p v -> Any p (Just v)

Hint: 

Uninhabited (Any p Nothing)

extract : Any p (Just x) -> p x

Visibility: public export

extractErased : Any p x -> Exists p

Visibility: public export

extractValue : Any p x -> (v : a ** p v)

Visibility: public export

app : (p x -> q y) -> Any p (Just x) -> Any q (Just y)

Visibility: export

mapProperty : (p x -> q x) -> Any p xs -> Any q xs

Visibility: public export