[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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 <[email protected]> > 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 >
