The Coq mailing list

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

Hi,

Notations work only if the module containing them is Imported.
That is the case for fun1.sigsig but not fun2.sigsig.

If you do it, the notation works for fun2.sigsig as well 
(but of course overrides the one for fun1.sigsig)

Jacek

On Mon, Jan 19, 2004 at 11:03:22AM +0100, Houda Anoun wrote:
> Hi ,
> Here is another problem with notations:
> 
> 
> Module Type SIGNot.
> Inductive InfTwoNat:nat-> Prop:=
> ohConstructorTooLong: forall (n:nat), InfTwoNat n.
> Notation "<<< n " :=(ohConstructorTooLong n  ) (at level 40):new_scope.
> End SIGNot.
> 
> Module sigImpl <:SIGNot.
> Inductive InfTwoNat:nat ->Prop:=
> ohConstructorTooLong: forall (n:nat), InfTwoNat n.
> 
> End sigImpl.
> 
> Module Type FUN.
> Declare Module sigsig :SIGNot.
> End FUN.
> Module Ext (picsou:SIGNot)<:FUN.
> Module sigsig:=picsou.
> End Ext.
> 
> 
> Module foufou(fun1:FUN)(fun2:FUN with Module sigsig:=fun1.sigsig).
> Open Scope new_scope.
> Import fun1.sigsig.
> Check (fun1.sigsig.ohConstructorTooLong O).
> 
> (* Coq < <<< 0
>      : InfTwoNat 0 
>  the notation works  :-) *)
> 
> 
> Check (fun2.sigsig.ohConstructorTooLong O).
> (* fun2.sigsig.ohConstructorTooLong 0
>      : fun2.sigsig.InfTwoNat 0 
>  it doesn't work  :-( *)
> 
> As we see both fun1.sigsig and fun2.sigsig are of type SIGNot where the 
> notation is defined...
> I think this problem results from the equivalence between modules which is 
> not supported by the current version of Coq...in fact we have 
> fun1.sigsig=fun2.sigsig ...
> Can this problem be solved ?!
> 
> 
> 
> 
> 
> 
> Pierre Casteran wrote:
> 
> > 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 !
> >
> >
> >
> >
> >
> >
> >
> >
> >
> >
> 
> 

--