- (>>>) : Monad m => ValidatorT m a b -> ValidatorT m b c -> ValidatorT m a c
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
- data 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
Constructor: - MkValidator : (a -> Result m b) -> ValidatorT m a b
- contramap : (a -> b) -> ValidatorT m b c -> ValidatorT m a c
Alter the input before validation using given function.
Totality: total- decide : Monad m => (t -> String) -> ((x : t) -> Dec (p x)) -> PropValidator m t p
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 : Monad m => ValidatorT m String Double
Verify that a string represents a decimal fraction.
Totality: total- equal : (DecEq t, Monad m) => (a : t) -> PropValidator m t (\b => a = b)
Verify that certain values are equal.
Totality: total- fail : Applicative m => String -> ValidatorT m a b
A validator which always fails with a given message.
Totality: total- fromMaybe : Monad m => (a -> String) -> (a -> Maybe b) -> ValidatorT m a b
Given a function converting a into Maybe b, build a Validator of a
converting it into b.
Totality: total- gtNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GT bound)
Verify that a Nat is strictly greate than a certain bound.
Totality: total- gteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip GTE bound)
Verify that a Nat is greater than or equal to certain bound.
Totality: total- integral : (Num a, (Neg a, Monad m)) => ValidatorT m String a
Verify whether a String represents an Integer
Totality: total- length : Monad m => (l : Nat) -> ValidatorT m (List a) (Vect l a)
Verify whether a list has a desired length.
Totality: total- ltNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LT bound)
Verify that a Nat is strictly less than a certain bound.
Totality: total- lteNat : Monad m => (bound : Nat) -> PropValidator m Nat (flip LTE bound)
Verify that a Nat is less than or equal to certain bound.
Totality: total- natural : Monad m => ValidatorT m String Nat
Verify whether a String represents a natural number.
Totality: total- validate : Validator a b -> a -> Either String b
Run validation within the Identity monad and unwrap result immediately.
Totality: total- validateT : ValidatorT m a b -> a -> Result m b
Run validation on given input, returning (Right refinedInput) if everything
is all right or (Left errorMessage) if it's not.
Totality: total- validator : (a -> Result m b) -> ValidatorT m a b
Given a function from input to Either String output, make a validator.
Totality: total- withError : Monad m => String -> ValidatorT m a b -> ValidatorT m a b
Replace validator's default error message.
Totality: total