Module Name Section

The Module keyword begins the module name section. The module name section must be the first section of every module header. Following this keyword is a string literal that specifies the local name of the module. The local name is a logical name, not a file system reference. As such it must match the file name, but must not include the .avail file extension. For example, a module named Foo must reside in a file whose name is Foo.avail, and its module name section should look like this:

Whitespace within a module header that does not occur within a string literal is deemed insignificant; it does not affect the meaning the module header. So Foo could also begin this way:

But the following is an illegal module name section for a module residing in Foo.avail, because it incorrectly declares the name of the module:

Local names occurring anywhere within a module header must never include a .avail file extension. Under usual circumstances, local names are resolved to file system paths via the standard module resolution mechanism.