Idris2Doc : Control.Validation

Control.Validation

Definitions

Result : (Type->Type) ->Type->Type
Totality: total
Visibility: public export
dataValidatorT : (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
Visibility: export
Constructor: 
MkValidator : (a->Resultmb) ->ValidatorTmab

Hints:
Monadm=>Alternative (ValidatorTma)
Monadm=>Applicative (ValidatorTma)
Functorm=>Functor (ValidatorTma)
Monadm=>Monad (ValidatorTma)
Validator : Type->Type->Type
Totality: total
Visibility: public export
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
Visibility: export
validate : Validatorab->a->EitherStringb
  Run validation within the Identity monad and unwrap result immediately.

Totality: total
Visibility: export
validator : (a->Resultmb) ->ValidatorTmab
  Given a function from input to Either String output, make a validator.

Totality: total
Visibility: export
withError : Monadm=>String->ValidatorTmab->ValidatorTmab
  Replace validator's default error message.

Totality: total
Visibility: export
fail : Applicativem=>String->ValidatorTmab
  A validator which always fails with a given message.

Totality: total
Visibility: export
(>>>) : Monadm=>ValidatorTmab->ValidatorTmbc->ValidatorTmac
  Compose two validators so that the second validates the output of the first.

Totality: total
Visibility: export
Fixity Declarations:
infixl operator, level 2
infixr operator, level 1
contramap : (a->b) ->ValidatorTmbc->ValidatorTmac
  Alter the input before validation using given function.

Totality: total
Visibility: export
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
Visibility: export
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
Visibility: export
natural : Monadm=>ValidatorTmStringNat
  Verify whether a String represents a natural number.

Totality: total
Visibility: export
integral : Numa=>Nega=>Monadm=>ValidatorTmStringa
  Verify whether a String represents an Integer

Totality: total
Visibility: export
double : Monadm=>ValidatorTmStringDouble
  Verify that a string represents a decimal fraction.

Totality: total
Visibility: export
length : Monadm=> (l : Nat) ->ValidatorTm (Lista) (Vectla)
  Verify whether a list has a desired length.

Totality: total
Visibility: export
equal : Monadm=>DecEqt=> (a : t) ->PropValidatormt (\b=>a=b)
  Verify that certain values are equal.

Totality: total
Visibility: export
lteNat : Monadm=> (bound : Nat) ->PropValidatormNat (flipLTEbound)
  Verify that a Nat is less than or equal to  certain bound.

Totality: total
Visibility: export
gteNat : Monadm=> (bound : Nat) ->PropValidatormNat (flipGTEbound)
  Verify that a Nat is greater than or equal to certain bound.

Totality: total
Visibility: export
ltNat : Monadm=> (bound : Nat) ->PropValidatormNat (flipLTbound)
  Verify that a Nat is strictly less than a certain bound.

Totality: total
Visibility: export
gtNat : Monadm=> (bound : Nat) ->PropValidatormNat (flipGTbound)
  Verify that a Nat is strictly greate than a certain bound.

Totality: total
Visibility: export