The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello, it seems that this is not possible. I am not sure why.

This is the closest solution I could find: Notice that Include can
avoid duplications in some cases.

Hope this helps,
Pierre

---------------------------------------------

Module Type m.
  Variable T :Set.
End m.

Module Type mt.
  Include m.
  Parameter foo : T -> T.
End mt.

Module Type mtt <: mt.
  Include m.
  Definition foo := (fun x:T => x).
End mtt.

------------- Another solution with typed functor: -----------


Module Type m.
  Variable T :Set.
End m.

Module Type mt(M:m).
  Include M.
  Parameter foo : T -> T.
End mt.

Module Type mtt(M:m)<: mt(M) with Definition foo:= (fun x:M.T => x).
  Include M.
  Definition foo := (fun x:M.T => x).
End mtt.



2014-04-21 21:53 GMT+02:00 Eddy Westbrook 
<westbrook AT kestrel.edu>:
> All,
>
> I asked this a while ago, but got no answer, so I am seeing if maybe I can 
> try again.
>
> The question: how can I write a “with” clause in a module type that refers 
> to a name already defined in the existing module type? That is, I want to 
> write something like
>
> Module Type mt’ := mt with Definition foo := fun (x:T) => x.
>
> where mt has the following definition:
>
> Module Type mt.
>   Parameter T : Set.
>   Parameter foo : T -> T.
> End mt.
>
> Or maybe there is some alternative way to update a name in a module type, 
> to give it a definition? Any suggestions?
>
> Thanks very much,
> -Eddy