Data.IMaybe

Version of Maybe indexed by an `isJust' boolean

Definitions

data IMaybe : Bool -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Just : a -> IMaybe True a

Nothing : IMaybe False a

Hints:

Applicative (IMaybe True)

Functor (IMaybe b)

Zippable (IMaybe b)

fromJust : IMaybe True a -> a

Totality: total
Visibility: public export