The Coq mailing list

[Matej Košík <matej.kosik AT inria.fr>]

Hi Talia,

On 12/01/2015 01:14 AM, Talia Ringer wrote:
> Thank you, all. I'm borrowing the book from another student, and I'll take 
> a look at the paper as well.
> 
> On the implementation side, is anyone familiar with where in the code to 
> start (particularly if I care about definitional equality),

Today I have created a small note about that:

  http://matej-kosik.github.io/www/doc/coq/hacking/getting_started.html

Among other things:
- how to debug coqtop
- where to put a breakpoint if you are interested in what happens after 
"Check ..." vernacular command

Let me please know if it helps or not.
(typechecking and stuff)

I'll be grateful for the feedback about usefulness of those notes.
(did it help you get started?)

I haven't read (yet) CPDT but according to the first section of the chapter 
you designated:
http://adam.chlipala.net/cpdt/html/Equality.html
those things makes sense. Chapter 4 of the Coq Reference Manual presents them 
under different names
(convertibility, subtyping, Conv-rule)

These are things that I presume must be tracable if you set a breakpoint to a 
"Check ..." command handler.

Cordially
---
Matej

> or is that a question better suited for the developers?
> 
> Thanks again,
> 
> Talia
> 
> On Sun, Nov 29, 2015 at 1:20 PM, Amirhossein Vakili 
> <avakili AT outlook.com
>  
> <mailto:avakili AT outlook.com>>
>  wrote:
> 
>     Hi Talia,
> 
>     With respect to CIC, I found "Type Theory and Formal Proof: An 
> Introduction" by Nederpelt and Geuvers very interesting.
> 
>     Cheers,
>     Amir
> 
> 
>     On 15-11-29 04:04 PM, Talia Ringer wrote:
>>     Hello,
>>
>>     I have a side project I'm doing for fun right now, and I'd like to 
>> learn more about the Coq metatheory (both the CIC metatheory and how it is 
>> implemented in Coq). In particular, I want to learn
>>     more about definitional equality in Coq, but I assume a whole-picture 
>> understanding is helpful. I've already read Adam Chlipala's post on 
>> equality
>>     <http://adam.chlipala.net/cpdt/html/Equality.html>. Now I would like 
>> to dig much deeper.
>>
>>     Are there any resources that may be helpful? From the CIC side, I am 
>> looking for some accessible introductory reading. From the Coq side, I am 
>> wondering where in the source code to dig; I've
>>     cloned the repository, but I don't know where to start. 
>>
>>     Thank you,
>>
>>     Talia
> 
>