[TYPES] How to code interesting examples in λC

[Beta Ziliani]

Thanks Herman and Randy! Very nice pointers to start with. I am still
failing to see how to properly encode the type of a vector, without
extrinsically defining a list with a proof of its size. But I admit I
haven't tried hard. In any case, your pointers suffice for my purpose now.



On Thu, Apr 11, 2019 at 6:42 PM R. Pollack <rpollack0 at gmail.com> wrote:

> Go to the source:
>
> Coquand and Huet, "Constructions: A Higher Order Proof System for
> Mechanizing Mathematics".
> Eurocal '85, LNCS 203
>
> --Randy
>
> On Thu, Apr 11, 2019 at 4:28 PM Beta Ziliani <beta.ziliani at gmail.com>
> wrote:
> >
> > [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> >
> > Hi,
> >
> > In a course I'm teaching, I wanted to show the Calculus of Constructions
> > (a.k.a. λC) prior to jumping to the Calculus of Inductive Constructions
> > (CIC). However, I find myself unable to code any interesting example. In
> > particular, I wasn't able to Church-encode a vector, a list with *n*
> > elements, whose *n* is defined in the type. Or, more primitively, the
> > equality type. Someone knows if this is possible to do, or send me
> pointers
> > at where such problem is discussed?
> >
> > Thanks,
> > Beta
>