The Coq mailing list

[���� <hskiowa AT kaist.ac.kr>]

Hello.

 

This is the first time I email to coq-club.

 

I am an undergradate student in Korea, and I have been recently using coq program for a few months.

 

Here are two questions:

 

1. Search commands do not search beyond definitions. I mean it doesn't go through delta reductions.

 

What should I do if I want to search for definitions related to a keyword?

 

2. There are many coq script files in a folder. They inherit among themselves using commands such as  "Require Import/Export blabla."

 

Is there a program to view a "genealogy tree" of the files? I think it would come in handy when compiling or adjusting files.

 

Is there a program to view a "genealogy tree" for definitions/theorems? This will be very useful, for instance, in figuring out how powerful an axiom/a theorem is.

 

 

Hyung Sun Kim

Department of Mathematical Sciences in KAIST