The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

Carlos.SIMPSON writes:
 > Hi. Has anybody tried using Coq to automatically generate theorems, and
 > say store them in a file? 

I do not  know of any such work.  Could you be a bit  more precise, by
the way:  would you  like to generate  theorems' proofs or  just their
statements; do you have a  syntax problem (I mean some difficulties in
generating Coq concrete syntax) or is your problem somewhere else?
 
 > Finally, a stupid question: how do you define a .coqrc file
 > on a PC windows 98? Windows doesnt allow filenames that start with `.'.

There is an option -init-file of Coq to specify the resource file.

Best regards,
-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr