The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Hmmm, I don't think there's much to point you at.

Maybe you will want to take a look at the paragraph "Recursive Type
Definitions" in this chapter of CPDT:
http://adam.chlipala.net/cpdt/html/DataStruct.html

This is a fixpoint encoding of homogeneous nested tuples (repeat) and
of finite natural numbers (index).
The latters allow you to safely index a position inside the formers.

The functions are then defined in a somewhat straightforward way:

first is a safe zero.
next is a safe successor function.
last builds (n - 1), the biggest safe index in a set of n elements.
lift lifts an index in a bigger set: it has the same value, but
indexes a set with an additional element.
select safely retrieves an element from a tuple.
eta_index is just some sort of eta-expansion for safely-indexed
collections apparently.

What is confusing you? Is it how these typecheck, what they define, or
the reason why they are defined this way? Or something else?

- Valentin

On Mon, Aug 12, 2013 at 5:36 PM, t x 
<txrev319 AT gmail.com>
 wrote:
> In the lambda tamer source, /src/coq/Util.v, there's the following block of
> code:
>
> https://gist.github.com/anonymous/76f36130b1bb9a2f6786
>
> I've played around with a few "Eval compute in ... "
>
> however, it's not clear to me what the intuitive definitions for:
> "first, next, last, lift, select, eta_index"
> are.
>
> Can someone point me at a paper/reference on the theoretical model behind
> this "tuple" ?
>
> Thanks!