qualifiedother

qualified sort/operator/parameter

CafeOBJ allows for using the same name for different sorts, operators, and parameters. One example is declaring the same sort in different modules. In case it is necessary to qualify the sort, operator, or parameter, the intended module name can be affixed after a literal .: <name>.<modname>

Example: In case the same sort Nat is declared in both the module SIMPLE-NAT and PANAT, one can use Nat.SIMPLE-NAT to reference the sort from the former module.

Furthermore, a similar case can arise when operators of the same name have been declared with different number of arguments. During operator renaming (see view) the need for qualification of the number of parameters might arise. In this case the number can be specified after an affixed /: <opname>/<argnr>

Related: qualified term, parameterized module