The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>]

> In Coq's kernel, we find two data types which are constr and kind of term,
> what's the difference between them??

 constr is the abstract datatype for the terms of CIC. All the functions
  that have terms as arguments/results use the constr type.

 kind_of_term is a view (in the sense of Wadler) used to pattern match over
  the abstract data type constr. The only way to obtain a kind_of_term is
  to apply the kind_of_term function over a constr. No other function should
  maniputale a kind_of_term. Thus you do not need a function from
  kind_of_term to constr, since you got the kind_of_term from
  (kind_of_term t) and you already have t that is of type constr.

 constr was made abstract (and the view kind_of_term added) to play with
 richer representations for the terms (e.g. with additional information in
 them to guide reduction, or with more sharing, etc.). Actually this is
 exploited only to force a bit of sharing in the terms, and the two data
 types are identical.

 To summarize: always manipulate arguments of type constr; use the
 kind_of_term function to perform pattern matching over constr.

                                        Hope it helps,
                                          C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------