The Coq mailing list

[t x <txrev319 AT gmail.com>]

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!