Data.Maybe.All

Definitions

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

Totality: total
Visibility: public export
Constructors:

Nil : All p Nothing

Value : p x -> All p (Just x)

.value : All p (Just x) -> p x

Visibility: export

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

Visibility: export

fromMaybe : ((x : a) -> p x) -> (m : Maybe a) -> All p m

Visibility: export

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

Visibility: public export