Currently we have the syntax module M = F { X } for giving the name M to the instantiation of the functor F with module parameter X. However we cannot simply do module M = N where N is a regular module, not a functor. Such a feature might be useful for exposing a deeply nested submodule, e.g. submodule M = submodule A::B::C::M. Alternatively if we have #1589 then this could be achieved by
Currently we have the syntax
module M = F { X }for giving the nameMto the instantiation of the functorFwith module parameterX. However we cannot simply domodule M = NwhereNis a regular module, not a functor. Such a feature might be useful for exposing a deeply nested submodule, e.g.submodule M = submodule A::B::C::M. Alternatively if we have #1589 then this could be achieved byor perhaps be syntactic sugar for it.