Idris2Doc : Data.Validated

Data.Validated

data IsValid : Validated e a -> Type
  Totality: total
  Constructor: 
ItIsValid : IsValid (Valid x)
data Validated : Type -> Type -> Type
  `Validated` is like an `Either` but accumulates all errors with semigroup operation.

  Totality: total
  Constructors:
  
Valid : a -> Validated e a
  
Invalid : e -> Validated e a
ValidatedL : Type -> Type -> Type
  Special case of `Validated` with a `List` as an error accumulator.

  Totality: total
fromEither : Either e a -> Validated e a
  Totality: total
fromEitherL : Either e a -> ValidatedL e a
  Totality: total
fromMaybe : Monoid e => Maybe a -> Validated e a
  Totality: total
isItValid : (v : Validated e a) -> Dec (IsValid v)
  Totality: total
oneInvalid : Applicative f => e -> Validated (f e) a
  Totality: total
toEither : Validated e a -> Either e a
  Totality: total
toMaybe : Validated e a -> Maybe a
  Totality: total