Idris2Doc : Search.Properties

Search.Properties

The content of this module is based on the paper
Applications of Applicative Proof Search
by Liam O'Connor
interfaceAProp : (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 : ListType
toProp : ta -> PropConstraintsa

Implementations:
AProp (Propcs)
APropHDec
APropDec
Constraints : APropt => ListType
Totality: total
Product : ListType -> Type
  Take the product of a list of types

Totality: total
recordProp : ListType -> 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 (Productcs) -> Fuel -> HDeca) -> Propcsa

Projection: 
.runProp : Propcsa -> Colist1 (Productcs) -> Fuel -> HDeca
  The function trying to find an `a` provided generators for `cs`.
Made total by consuming some fuel along the way.
check : {autogen : 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 : {autoaPropt : 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 : APropt => ta -> PropConstraintsa
Totality: total