The Coq mailing list

["Devisschere Yann" <devissch AT enseirb.fr>]

First, I would thank Claudio Sacerdoti Cohen for his former answer.

I still have got a problem :
I wanted to edit the kind_of_term corresponding to my definition and the
lemma in order to have a better vision of the differences. Thanks to his
explanation I succeed in editing the kind_of_term associated to the constant
definition nevertheless, I can't get the kind_of_term associated to the
lemma while I don't manage its proof... And when I work on the constant
lemma with its proof, I have a complete decomposotion of the single LTac
tactic what make the constant difficult to read and don't allow me to do a
clear link between the definition and the introduction of the lemma. I think
my problem is simple : while not proved, the lemma is not yet a constant...
What type of data is it and then how to access to its kind_of_term ? Then I
also would like to know how to declare such an object in ml in order to let
coq know the introduction of the lemma and then allow the coq-user prove it.


(Ex :
Definition K2Diam (i:I) (j:J) : strucrule I J :=
((pdiam j (pcomma i (pvar 1) (pvar 2))),
 (pcomma i (pvar 1) (pdiam j (pvar 2)))).
=>
generate the lemma declaration
=>
Lemma K2DIAM_rw:forall decI decJ A W (t1 t2 : context I J A W) (i:I) (j:J),
   (apply_rule (K2Diam i j) decI decJ (TDiamond j (Comma i t1 t2))) =
   Some (Comma i t1 (TDiamond j t2)).
)

Yann Devisschere