Data.Validated

Definitions

data Validated : Type -> Type -> Type

  `Validated` is like an `Either` but accumulates all errors with semigroup operation.

Totality: total
Visibility: public export
Constructors:

Valid : a -> Validated e a

Invalid : e -> Validated e a

Hints:

Monoid e => Alternative (Validated e)

Semigroup e => Applicative (Validated e)

Bifoldable Validated

Bifunctor Validated

Bitraversable Validated

(DecEq e, DecEq a) => DecEq (Validated e a)

(Eq e, Eq a) => Eq (Validated e a)

Foldable (Validated e)

Functor (Validated e)

Injective Valid

Injective Invalid

Monoid e => Monoid (Validated e a)

Semigroup e => Semigroup (Validated e a)

(Show e, Show a) => Show (Validated e a)

Traversable (Validated e)

Uninhabited (Valid x = Invalid e)

Uninhabited (Invalid e = Valid x)

Semigroup e => Zippable (Validated e)

ValidatedL : Type -> Type -> Type

  Special case of `Validated` with a `List1` as an error accumulator.

Totality: total
Visibility: public export

oneInvalid : Applicative f => e -> Validated (f e) a

Totality: total
Visibility: public export

fromEither : Either e a -> Validated e a

Totality: total
Visibility: public export

fromEitherL : Either e a -> ValidatedL e a

Totality: total
Visibility: public export

toEither : Validated e a -> Either e a

Totality: total
Visibility: public export

fromMaybe : Monoid e => Maybe a -> Validated e a

Totality: total
Visibility: public export

toMaybe : Validated e a -> Maybe a

Totality: total
Visibility: public export

data IsValid : Validated e a -> Type

Totality: total
Visibility: public export
Constructor: 

ItIsValid : IsValid (Valid x)

Hint: 

Uninhabited (IsValid (Invalid e))

isItValid : (v : Validated e a) -> Dec (IsValid v)

Totality: total
Visibility: public export