Idris2Doc : Search.Generator

Search.Generator

The content of this module is based on the paper
Applications of Applicative Proof Search
by Liam O'Connor

The main difference is that we use `Colist1` for the type of
generators rather than `Stream`. This allows us to avoid generating
many duplicates when dealing with finite types which are common in
programming (Bool) but even more so in dependently typed programming
(Vect 0, Fin (S n), etc.).
interfaceGenerator : Type -> Type
  A generator for a given type is a non-empty colist of values of that
type.

Parameters: a
Methods:
generate : Colist1a

Implementations:
GeneratorNat
GeneratorBool
Generator (Fin (Sn))
Generatora => Generator (a, ())
(Generatora, Generatorb) => Generator (a, b)
{0 b : a -> Type} -> (Generatora, (x : a) -> Generator (bx)) => Generator (DPaira (\x => bx))
Generatora => Generator (Vectna)
Generatora => Generator (Lista)
generate : Generatora => Colist1a