Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] problem with notations

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem with notations


chronological Thread 
  • From: Pierre Casteran <casteran AT labri.fr>
  • To: Jevgenijs Sallinens <jevgenijs AT dva.lv>
  • Cc: Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>, Jacek Chrzaszcz <chrzaszc AT mimuw.edu.pl>, coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] problem with notations
  • Date: Thu, 15 Jan 2004 17:26:55 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
  • Organization: LaBRI

Jevgenijs Sallinens wrote:


If these problems are real, I think the usage of inductive definitions
in module types are not reliable for large projects.
Instead in module types there should placed only properties
of such definitions,but definitions themselves should be
within implementation modules.


Do you mean to put in the module types such informations as
_ind, _rec, _rect constructions, equalities related to iota-reductions
and so on ? That can be a lot of information to write.

Pierre



--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran









Archive powered by MhonArc 2.6.16.

Top of Page