Idris2Doc : Search.Generator

Search.Generator(source)

The content of this module is based on the paper
Applications of Applicative Proof Search
by Liam O'Connor
https://doi.org/10.1145/2976022.2976030

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.).

Definitions

interface Generator : Type -> Type

  A generator for a given type is a non-empty colist of values of that
  type.

Parameters: a
Methods:

generate : Colist1 a

Implementations:

Generator Nat
Generator Bool
Generator (Fin (S n))
Generator a => Generator (a, ())
(Generator a, Generator b) => Generator (a, b)
{0 b : a -> Type} -> (Generator a, (x : a) -> Generator (b x)) => Generator (x : a ** b x)
Generator a => Generator (Vect n a)
Generator a => Generator (List a)

generate : Generator a => Colist1 a

Visibility: public export