Idris2Doc : Control.Validation


(>>>) : Monadm => ValidatorTmab -> ValidatorTmbc -> ValidatorTmac
Compose two validators so that the second validates the output of the first.
Totality: total
Fixity Declaration: infixl operator, level 2
Result : (Type -> Type) -> Type -> Type
Totality: total
Validator : Type -> Type -> Type
Totality: total
ValidatorT : (Type -> Type) -> Type -> Type -> Type
Validators in this module come in two flavours: Structural Validators and
Property Validators. They are both wrappers around functions which take
some input and confirm that it's valid (returning some witness of its
validity) or fail with an error described by a string.
Totality: total
MkValidator : (a -> Resultmb) -> ValidatorTmab
contramap : (a -> b) -> ValidatorTmbc -> ValidatorTmac
Alter the input before validation using given function.
Totality: total
decide : Monadm => (t -> String) -> ((x : t) -> Dec (px)) -> PropValidatormtp
Given a value x and a decision procedure for property p, validateT if p x
holds, returning a proof if it does. The procedure also has access to the
raw input in case it was helpful.
Totality: total
double : Monadm => ValidatorTm String Double
Verify that a string represents a decimal fraction.
Totality: total
equal : (DecEqt, Monadm) => (a : t) -> PropValidatormt (\b => a = b)
Verify that certain values are equal.
Totality: total
fail : Applicativem => String -> ValidatorTmab
A validator which always fails with a given message.
Totality: total
fromMaybe : Monadm => (a -> String) -> (a -> Maybeb) -> ValidatorTmab
Given a function converting a into Maybe b, build a Validator of a
converting it into b.
Totality: total
gtNat : Monadm => (bound : Nat) -> PropValidatormNat (flipGTbound)
Verify that a Nat is strictly greate than a certain bound.
Totality: total
gteNat : Monadm => (bound : Nat) -> PropValidatormNat (flipGTEbound)
Verify that a Nat is greater than or equal to certain bound.
Totality: total
integral : (Numa, (Nega, Monadm)) => ValidatorTm String a
Verify whether a String represents an Integer
Totality: total
length : Monadm => (l : Nat) -> ValidatorTm (Lista) (Vectla)
Verify whether a list has a desired length.
Totality: total
ltNat : Monadm => (bound : Nat) -> PropValidatormNat (flipLTbound)
Verify that a Nat is strictly less than a certain bound.
Totality: total
lteNat : Monadm => (bound : Nat) -> PropValidatormNat (flipLTEbound)
Verify that a Nat is less than or equal to certain bound.
Totality: total
natural : Monadm => ValidatorTm String Nat
Verify whether a String represents a natural number.
Totality: total
validate : Validatorab -> a -> Either String b
Run validation within the Identity monad and unwrap result immediately.
Totality: total
validateT : ValidatorTmab -> a -> Resultmb
Run validation on given input, returning (Right refinedInput) if everything
is all right or (Left errorMessage) if it's not.
Totality: total
validator : (a -> Resultmb) -> ValidatorTmab
Given a function from input to Either String output, make a validator.
Totality: total
withError : Monadm => String -> ValidatorTmab -> ValidatorTmab
Replace validator's default error message.
Totality: total