Data.Enumerate.Indexed(source)

The content of this module is based on the paper
A Completely Unique Account of Enumeration
by Cas van der Rest, and Wouter Swierstra
https://doi.org/10.1145/3547636

Definitions

record IEnumerator : (i -> Type) -> Type -> Type

  An (a,b)-enumerator is an enumerator for values of type b provided
  that we already know how to enumerate subterms of type a

Totality: total
Visibility: export
Constructor: 

MkIEnumerator : (((v : i) -> List (a v)) -> List b) -> IEnumerator a b

Projection: 

.runIEnumerator : IEnumerator a b -> ((v : i) -> List (a v)) -> List b

Hints:

Alternative (IEnumerator a)

Applicative (IEnumerator a)

Functor (IEnumerator a)

Monad (IEnumerator a)

rec : (v : i) -> IEnumerator a (a v)

Totality: total
Visibility: export

pairWith : (b -> c -> d) -> IEnumerator a b -> IEnumerator a c -> IEnumerator a d

Totality: total
Visibility: export

pair : IEnumerator a b -> IEnumerator a c -> IEnumerator a (b, c)

Totality: total
Visibility: export

sig : {b : a -> Type} -> IEnumerator f a -> ((x : a) -> IEnumerator f (b x)) -> IEnumerator f (x : a ** b x)

Totality: total
Visibility: export

const : List b -> IEnumerator a b

Totality: total
Visibility: export

isized : ((v : i) -> IEnumerator a (a v)) -> Nat -> (v : i) -> List (a v)

Totality: total
Visibility: export

indexed : (d : (i -> IDesc List i)) -> (v : i) -> IEnumerator (Fix d) (Fix d v)

Totality: total
Visibility: export

0 Memorator : (d : Desc p) -> (Fix d -> Type) -> Type -> Type

Totality: total
Visibility: export

memorate : ((x : Fix d) -> Memorator d b (b x)) -> Nat -> (x : Fix d) -> List (b x)

Totality: total
Visibility: export