The Coq mailing list

[Jacek Chrzaszcz <chrzaszc AT mimuw.edu.pl>]

On Tue, Jan 13, 2004 at 02:00:16PM +0100, Pierre Casteran wrote:
> 
> There is a slight problem. This work only if we work with opaque
> signature constraint , and not if I use '<:'
> 

Yes. That is also a feature ;)

The "<:" transparent signature constraint is only there to make sure that
the module has the right signature (and for documentation).
It changes nothing for typing and "extra-logical" stuff like notations etc.

One might of course try to use the notations included in the signature, but
then another problem arises. What about:

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

Module M1  <: S1.
  Inductive  P : Set :=
    c : P .
  Notation "'X'" := c  (at level 40) : my_scope.
End M1.

 
Import M1.

Open Scope my_scope.

Print c.


(*
Now what: XXXXXXXXXXXXXXX or X ?
*)


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

Yes, it is OK. Apart from having to write everything twice (and making Coq
verify that the declaration and definitions correspond) I can see no
problem. 

BTW: I am thinking about implementing some "Include from signature"
command but I am not sure what it will precisely be and (even less) when
this will be available.

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

Thank you very much!


Jacek

PS. I hope I will have some time to hack at last!