Scope management

Require, Import, Export

TODO

local, global, export

TODO

Module, Module Type

TODO

Section

TODO

Context

TODO

Notation

TODO