Idris2Doc : Data.Validated

Data.Validated

Definitions

dataValidated : Type->Type->Type
  `Validated` is like an `Either` but accumulates all errors with semigroup operation.

Totality: total
Visibility: public export
Constructors:
Valid : a->Validatedea
Invalid : e->Validatedea

Hints:
Monoide=>Alternative (Validatede)
Semigroupe=>Applicative (Validatede)
BifoldableValidated
BifunctorValidated
BitraversableValidated
(DecEqe, DecEqa) =>DecEq (Validatedea)
(Eqe, Eqa) =>Eq (Validatedea)
Foldable (Validatede)
Functor (Validatede)
InjectiveValid
InjectiveInvalid
Monoide=>Monoid (Validatedea)
Semigroupe=>Semigroup (Validatedea)
(Showe, Showa) =>Show (Validatedea)
Traversable (Validatede)
Uninhabited (Validx=Invalide)
Uninhabited (Invalide=Validx)
Semigroupe=>Zippable (Validatede)
ValidatedL : Type->Type->Type
  Special case of `Validated` with a `List` as an error accumulator.

Totality: total
Visibility: public export
oneInvalid : Applicativef=>e->Validated (fe) a
Totality: total
Visibility: public export
fromEither : Eitherea->Validatedea
Totality: total
Visibility: public export
fromEitherL : Eitherea->ValidatedLea
Totality: total
Visibility: public export
toEither : Validatedea->Eitherea
Totality: total
Visibility: public export
fromMaybe : Monoide=>Maybea->Validatedea
Totality: total
Visibility: public export
toMaybe : Validatedea->Maybea
Totality: total
Visibility: public export
dataIsValid : Validatedea->Type
Totality: total
Visibility: public export
Constructor: 
ItIsValid : IsValid (Validx)

Hint: 
Uninhabited (IsValid (Invalide))
isItValid : (v : Validatedea) ->Dec (IsValidv)
Totality: total
Visibility: public export