coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] problem with notations, Houda Anoun
- Re: [Coq-Club] problem with notations,
Jacek Chrzaszcz
- Re: [Coq-Club] problem with notations,
Pierre Casteran
- Re: [Coq-Club] problem with notations, Jacek Chrzaszcz
- Re: [Coq-Club] problem with notations,
Houda Anoun
- Re: [Coq-Club] problem with notations, Jacek Chrzaszcz
- Re: [Coq-Club] problem with notations,
Pierre Casteran
- <Possible follow-ups>
- Re: [Coq-Club] problem with notations,
Jevgenijs Sallinens
- Re: [Coq-Club] problem with notations, Pierre Courtieu
- Re: [Coq-Club] problem with notations, Houda Anoun
- Re: [Coq-Club] problem with notations,
Jevgenijs Sallinens
- Re: [Coq-Club] problem with notations, Pierre Casteran
- Re: [Coq-Club] problem with notations, Jacek Chrzaszcz
- Re: [Coq-Club] problem with notations, Jevgenijs Sallinens
- Re: [Coq-Club] problem with notations, Jevgenijs Sallinens
- Re: [Coq-Club] problem with notations,
Jacek Chrzaszcz
Archive powered by MhonArc 2.6.16.