The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-08-11 8:37 GMT+02:00 N. Raghavendra <raghu AT hri.res.in>:

At 2015-08-10T10:24:52Z, Soegtrop, Michael wrote:

> maybe there is a more elegant way, but what I did sometimes in such
> cases is to wrap it into a module like this:
>
>       Module L.
>       Require List.
>       Include List.
>       End L.
>
>       Print L.hd.

Thanks for the suggestion.  Meanwhile, I found that

  Require LongModuleName.
  Module LMN := LongModuleName.
  Print LMN.foo.

also works.  Is there any reason to prefer the one over the other?

​Your way seems better to me:

* shorter to write (not much, but still a gain)

* clearer syntax

* less keywords to memorize (not much, but still a gain)

* I am not sure how memory management is done,

  but I guess your way is more efficient as LongModuleName

  and LMN should be able to share a common data structure,

  while "Include" might require a copy, since you can add

  other definitions to the module before closing it, and
  thus "modify" the module (so sharing is less evident to be done).​

 

Cheers,
Raghu.

--
N. Raghavendra <raghu AT hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/