Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] constr and kind_of_term??!

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] constr and kind_of_term??!


chronological Thread 
  • From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>
  • To: anoun AT labri.fr
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] constr and kind_of_term??!
  • Date: Fri, 8 Apr 2005 16:53:09 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page