Data.Maybe0

Definitions

data Maybe0 : Type -> Type

  An optional data type for erased values.
  At runtime, this is just 0 or 1.

Totality: total
Visibility: public export
Constructors:

Nothing0 : Maybe0 a

Just0 : (0 _ : a) -> Maybe0 a

isJust : Maybe0 a -> Bool

Totality: total
Visibility: public export

map : (0 _ : (a -> b)) -> Maybe0 a -> Maybe0 b

Totality: total
Visibility: public export

data IsJust0 : Maybe0 a -> Type

Totality: total
Visibility: public export
Constructor: 

ItIsJust0 : IsJust0 (Just0 v)

0 fromJust0 : (m : Maybe0 a) -> IsJust0 m => a

Totality: total
Visibility: public export

(<|>) : Maybe0 t -> Lazy (Maybe0 t) -> Maybe0 t

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 2

zipWith : (0 _ : (a -> b -> c)) -> Maybe0 a -> Maybe0 b -> Maybe0 c

Totality: total
Visibility: public export

zipWith3 : (0 _ : (a -> b -> c -> d)) -> Maybe0 a -> Maybe0 b -> Maybe0 c -> Maybe0 d

Totality: total
Visibility: public export

maybeCong : (f : (a -> b)) -> Maybe0 (x = y) -> Maybe0 (f x = f y)

Totality: total
Visibility: public export

maybeCong2 : (f : (a -> b -> c)) -> Maybe0 (x = y) -> Maybe0 (v = w) -> Maybe0 (f x v = f y w)

Totality: total
Visibility: public export