The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Jacek Chrzaszcz wrote:
> On Mon, Jan 12, 2004 at 01:03:15PM +0100, Houda Anoun wrote:

> Seriously, in situations like this one:
> Module M:T:=A
> one has to decide which elements come from T and which from A.
> Now they simply all come from T.


There is a slight problem. This work only if we work with opaque
signature constraint , and not if I use '<:'

Module Type S1.
Inductive  P : Set :=
  c : P.
  Notation "'XXX'" := c  (at level 40) : my_scope.
End S1.

Module M1  <: S1.
 Inductive  P : Set :=
 c : P .
End M1.


Import M1.

(* Open Scope my_scope.
 Error: Scope my_scope is not declared *)


If I use a constraint with ':', the notation is available :

Module M2 : S1.
  Inductive  P : Set :=
 c : P .
End M2.

Import M2.

Open Scope my_scope.

Check c.

(*
 XXX : P
*)

By the way, I have often to deal with inductive type definitions.
Is it OK to put the inductive definition in the signature (since
it is a declaration of the constructors and the _ind, _rec, ...
theorems), and duplicate the inductive definition in the signature
and in the module and/or functor ?.

Pierre

P.S.
 Jacek, Igor (Walukiewicz) told me about your thesis. Congratulations !










--
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