The Coq mailing list

[Milad Ketabii <ketabii.math AT gmail.com>]

Hi Sylvian

There is no functors here. Neither base nor any of the modules depending on it are parametric modules.

The Base itself is a module, which has some sections and other smaller modules in it.

To clarify the situation further, let's name the modules which depend on the Base by M1, M2, so forth. Also assume that Good_Person is a definition in M1, where two functions f1 and f2 each of which is defined in Base, are used to specify the Good_Person property.

The problem is that I need to use the name of Base in front of f1 and f2 at each instance by writing Base.f1 and Base.f2 . What I want is to simply write f1 and f2 wherever I wish and go through no problem. 

The situation would be like this; when one calls the Coq library for lists inside their modules/sections/etc for formalising something

, they would not use the name List.hd or List.tl in each instance of using the head and tail functions defined in Coq.List.list. They would rather simply write hd or tl in their specification.

I hope it is clearer what I mean. If otherwise, then let me know so that I lead to my github link.

thanks for your help,

Milad

On Wed, Jun 6, 2018 at 5:27 PM, Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr> wrote:

Hi Milad,

Le 06/06/2018 à 07:50, Milad Ketabii a écrit :

Hi there!

I have a problem, for which a solution already is there. However, I am looking for a better way of accomplishing the task.

Here, I will first explain the problem itself, as much simply as possible. Then I mention the crazy solution which I have. But I hope someone would kindly hint at a superior approach.

*The problem and a crazy solution:*

I have a formalisation which I intend to break into a base file and some modules, each of which calls this base in.

The base formalisation has variables. These variables are used inside each module as well. We finally would extract executable program into Haskell.

The base is constituted of some sections. To make the variables in the base file available to the modules (without instantiating them), I have made the out-most part of the base file as a module, rather than a section. This prevents errors that I would get by trying to compile the modules.

I do not fully understand your current solution: is this "out-most" part a module in parameter of each module ? (Now, are your modules actually functors ?)

However, the hassle is that I need to put the name of the base module in front of every variable, definition, and function which are celled in the modules.

Whatever module "Base" is: a parameter or an actual implementation, you only need to write "Import Base." in each module that uses "Base" in order to solve your problem.

Regards,

Sylvain.