parameterizedmodule

parameterized module

A module with a parameter list (see module) is a parameterized module. Parameters are given as a comma (,) separated list. Each parameter is of the form [ <import_mode> ] <param_name> :: <module_name> (spaces around :: are obligatory).

The parameter's module gives minimal requirements on the module instantiation.

Within the module declaration sorts and operators of the parameter are qualified with .<parameter_name> as seen in the example below.

Related: qualified sort

Example

mod* C {
  [A]
  op add : A A -> A .
}
mod! TWICE(X :: C) {
  op twice : A.X -> A.X .
  eq twice(E:A.X) = add.X(E,E) .
}