- interface 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 : t a -> Prop Constraints a
Implementations:
- AProp (Prop cs)
- AProp HDec
- AProp Dec
- Constraints : AProp t => List Type
- Totality: total
- Product : List Type -> Type
Take the product of a list of types
Totality: total- record 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: - MkProp : (Colist1 (Product cs) -> Fuel -> HDec a) -> Prop cs a
Projection: - .runProp : Prop cs a -> Colist1 (Product cs) -> Fuel -> HDec a
The function trying to find an `a` provided generators for `cs`.
Made total by consuming some fuel along the way.
- check : {auto gen : Generator (Product cs)} -> (f : Fuel) -> (p : Prop cs a) -> So (isTrue (runProp p generate f)) => a
We can run an AProp to try to generate a value of type a
Totality: total- exists : {auto aPropt : AProp t} -> ((x : a) -> t (p x)) -> Prop (a :: Constraints) (DPair a p)
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 : AProp t => t a -> Prop Constraints a
- Totality: total