Allow files without top module

[UlfNorell]

From andreas....@gmail.com on November 12, 2013 14:59:29

For throw-away Agda files, I would like to be able to omit the

module JustAThrowAwayFileButModuleNameMustMatchFileNameExactly where

top-level module declaration.

Use cases:

• little bits of Agda code in a presentation
• test suite
• playing, experimentation and demonstration

If no module name is encounterd before the first non-import statement, just the (unqualified) file name is taken as module name.

Original issue: http://code.google.com/p/agda/issues/detail?id=953

[UlfNorell]

From ulf.nor...@gmail.com on November 13, 2013 02:53:15

Allows either omitting the top-level module or defining it as module _ where.

Status: Fixed

[UlfNorell]

From andres.s...@gmail.com on November 13, 2013 04:27:14

After the patches, the following module doesn't type-check:

module Foo where

$ agda Foo.agda ... Parse error Foo where ...

Status: Accepted

[UlfNorell]

From nils.anders.danielsson on November 13, 2013 08:26:18

Owner: ulf.nor...@gmail.com
Labels: -Type-Enhancement Type-Defect Milestone-2.3.4 Priority-High

[UlfNorell]

From ulf.nor...@gmail.com on November 13, 2013 12:34:36

That's by design. Put a space before the where. The top-level is now in a layout context, which makes the syntax more consistent than before (you couldn't write a local module like that before).

Status: Fixed