Basic principles

Our module system strongly uses the notion of names. Any objects (theorems, terms, ...) has a distinct name. Therefore, if you want to merge two modules which both declare an object with the same name, this two objects must coincide after merging.

Here are the conditions under which two objects can coincide:

• They must have the same sorts. A formula can not coincide with a natural number.
• If both objects are defined expressions, their definitions must be structurally equal.
• If both objects are theorems or axioms, they must have structurally equal conclusions. They do not need to have the same proof.

If one of this condition is not respected, the loading of modules will fail.

These rules allow you to make coincide an axiom with a theorem and a constant with a definition. This is why we can prove axiomatic properties of a structure like groups by adding some constants and axioms and then use this module on a particular group where the axioms may be proven and the constants may already exists.