select

select <mod_exp> .

Selects a module given by the module expression <mod_exp> as the current module. All further operations are carried out within the given module. In contrast to open this does not allow for modification of the module, e.g., addition of new sorts etc.

Related: module expression, open