Idris2Doc : Search.Properties

Search.Properties

AProp : (Type -> Type) -> Type
A type constructor satisfying the AProp interface is morally a Prop
It may not make use of all of the powers granted by Prop, hence the
associated `Constraints` list of types.
Parameters: t
Methods:
Constraints : List Type
toProp : ta -> PropConstraintsa

Implementations:
AProp (Propcs)
APropHDec
APropDec
Constraints : APropt => List Type
Totality: total
Product : List Type -> Type
Take the product of a list of types
Totality: total
Prop : List Type -> Type -> Type
A property amenable to testing
@cs is the list of generators we need (inferrable)
@a is the type we hope is inhabited
NB: the longer the list of generators, the bigger the search space!
Totality: total
Constructor: 
check : {auto gen : Generator (Productcs)} -> (f : Fuel) -> (p : Propcsa) -> So (isTrue (runProppgeneratef)) => a
We can run an AProp to try to generate a value of type a
Totality: total
exists : {auto aPropt : APropt} -> ((x : a) -> t (px)) -> Prop (a::Constraints) (DPairap)
Provided that we know how to generate candidates of type `a`, we can look
for a witness satisfying a given predicate over `a`.
Totality: total
toProp : {auto __con : APropt} -> ta -> PropConstraintsa
Totality: total