The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Wed, 09 Dec 2009 16:36:27 +0100, Christian Doczkal  
<doczkal AT ps.uni-sb.de> a écrit:

> I just stumbled across the following:
>
> Module Type S.
>   Parameter X : Type.
> End S.
>
> Module False : S.
>   Inductive X := .
> End False.
>
> (* Error: The kernel does not recognize yet that a parameter can be
> instantiated by an inductive type. Hint: you can rename the inductive
> type and give a definition to map the old name to the new name. *)
>
> (* Of course one can circumvent the problem like this, but it removes a
> lot of the structuring effect one would like Modules to have ...
>
> Inductive FalseT : Type := .
>
> Module FT : S.
>   Definition X := FalseT.
>   Definition R := @eq FalseT.
> End FT.


> Is there any work being done on the subject?
> Are there any theoretical issues?
I agree with you that the False module should be accepted;
about the structuring, it is not clear that it is really a problem.


 Module FT : S.
   Inductive FalseT : Type := .
   Definition X := FalseT.
   Definition R := @eq FalseT.
 End FT.

Note that you won't be able to acces the R field... as it doesn't appear  
in the signature of S.

If you want to know the structure of X outside FT (for your structuring  
problems), use rather:

Module FT : S with Definition X := FalseT.
   Definition X := FalseT.
   Definition R := @eq FalseT.
End FT.


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay