Introduction to PSF

Parameters

A parameters section must appear as the first section in a module and has the following layout.
    parameters
        Parameter
        begin
            sorts
                ...
            functions
                ...
            atoms
                ...
            processes
                ...
            sets
                ...
        end
        ...
Upon import of a module with parameters, a parameter can be bound to a module while all objects listed in the parameter are bound to actual objects from this module. Unbound parameters are inherited by the importing module and become parameters of this module. A parameter binding has the following layout.
    imports
        Module1 {
            Parameter bound by [
                a -> b,
                ...
            ] to Module2
        }