[TYPES] How to code interesting examples in λC

[Herman Geuvers]

Hi Beta,

For my proving with Computer Assistance course I let the students do 
higher order logic exercises in the Calculus of Constructions.
Define Leibniz equality and prove properties, define the transitive 
closure and prove properties etc.
See http://www.cs.ru.nl/~herman/onderwijs/provingwithCA/exercises10.pdf

Best

Herman

On 4/11/19 5:08 PM, Beta Ziliani 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
>