TyRE.Extra.Reflects

Definitions

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

Totality: total
Visibility: public export
Constructors:

Indeed : p x -> Reflects p (Just x)

Otherwise : ((x : a) -> Not (p x)) -> Reflects p Nothing

record RMaybe : (a -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

Because : (Holds : Maybe a) -> (0 _ : Reflects p Holds) -> RMaybe p

Projections:

.Holds : RMaybe p -> Maybe a

0 .Proof : ({rec:0} : RMaybe p) -> Reflects p (Holds {rec:0})

.Holds : RMaybe p -> Maybe a

Visibility: public export

Holds : RMaybe p -> Maybe a

Visibility: public export

0 .Proof : ({rec:0} : RMaybe p) -> Reflects p (Holds {rec:0})

Visibility: public export

0 Proof : ({rec:0} : RMaybe p) -> Reflects p (Holds {rec:0})

Visibility: public export

map : p <-> q -> RMaybe p -> RMaybe q

Visibility: public export

findR : (pred : (a -> Bool)) -> (xs : List a) -> RMaybe (\x => (Elem x xs, pred x = True))

Visibility: public export