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