Multiple modules in one file

Warning: this mode can not be used with XEmacs interface and in general in interactive mode ! To use it, develop the last module in interactive mode as one file and add it at the end of the main file when it works.

This feature will probably disappear soon ....

It is sometimes necessary to develop many small modules. It is possible in this case to group the definitions in the same file using the following syntax:

Module name1.
  ...
  ...
end.

Module name2.
  ...
  ...
end.

...

If the file containing these modules is named foo this is equivalent to having many files foo.name1.phx, foo.name2.phx, ...containing the definitions in each module. Therefore the name of each module (to be used with Import or Use) will be foo.name1, foo.name2, ....

Moreover, a module can use the previously defined modules in the same file using only the name of the module (omitting the file name).

Here is an example where we define semi-groups and homomorphisms.

Module semigroup.
  Sort g.
  Cst G : g -> prop.
  Cst rInfix[3] x "op" y : g -> g -> g.

  claim op_total /\x,y:G  G (x op y).
  new_intro -t total op_total.

  claim assoc /\x,y,z:G  x op (y op z) = (x op y) op z.
  new_equation -b assoc.

end.

Module homomorphism.

  Use semigroup with
    _ -> _.D
  .

  Use semigroup with
    _ -> _.I
  .

  Cst f : g -> g. 

  claim totality.f /\x:G.D  G.I (f x).
  new_intro -t f totality.f.

  claim compatibility.f /\x1,x2:G.D  f (x1 op.D x2) = f x1 op.I f x2.
  new_equation compatibility.f.

end.