The Coq mailing list

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

Hello,

anoun AT labri.fr
 writes:
 > In Coq's kernel, we find two data types which are constr and kind of term,
 > what's the difference between them??

Internally, there is no difference: the two types are equal (see
term.ml). But one is abstract (constr) and the other is not.

The type and function kind_of_term are provided to allow
pattern-matching on type constr (this is a ``view'' to speak
pedantically).

But constr remains abstrac so that we can maintain invariants (such as
``an application always has at least one argument'' and so on).

 > If we have a constr c, we can obtain it's kind of term using
 > (kind_of_term c), can we do the opposite? i.e. build a constr using
 > a kind-of-term?? 

No, because it would break the abstractness of type constr. You have
to use the constructor functions (mkVar, mkProd, ...) instead, but
this is rather immediate since the arguments of the kind_of_term
constructors are of type constr.

Hope this helps,
-- 
Jean-Christophe