Data.Either0

Definitions

data Either0 : Type -> Type -> Type

  A choice of two erased values.
  At runtime, this is just 0 or 1.

Totality: total
Visibility: public export
Constructors:

Left0 : (0 _ : a) -> Either0 a b

Right0 : (0 _ : b) -> Either0 a b

bimap : (0 _ : (a -> c)) -> (0 _ : (b -> d)) -> Either0 a b -> Either0 c d

  This is the identity at runtime.

Totality: total
Visibility: public export

map : (0 _ : (b -> d)) -> Either0 a b -> Either0 a d

  This is the identity at runtime.

Totality: total
Visibility: public export

0 either0 : (a -> e) -> (b -> e) -> Either0 a b -> e

Totality: total
Visibility: public export

data IsLeft0 : Either0 a b -> Type

Totality: total
Visibility: public export
Constructor: 

ItIsLeft0 : IsLeft0 (Left0 v)

0 fromLeft0 : (e : Either0 a b) -> IsLeft0 e => a

Totality: total
Visibility: public export

data IsRight0 : Either0 a b -> Type

Totality: total
Visibility: public export
Constructor: 

ItIsRight0 : IsRight0 (Right0 v)

0 fromRight0 : (e : Either0 a b) -> IsRight0 e => b

Totality: total
Visibility: public export

(<|>) : Either0 a b -> Lazy (Either0 a b) -> Either0 a b

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