coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Valentin Robert <valentin.robert.42 AT gmail.com>
- To: t x <txrev319 AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple"
- Date: Mon, 12 Aug 2013 17:56:28 +0100
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!
- [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple", t x, 08/12/2013
- Re: [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple", Valentin Robert, 08/12/2013
- Re: [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple", t x, 08/12/2013
- Re: [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple", Valentin Robert, 08/12/2013
- Re: [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple", t x, 08/12/2013
- Re: [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple", Valentin Robert, 08/12/2013
Archive powered by MHonArc 2.6.18.