[Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1

Nils Anders Danielsson nad at cse.gu.se
Wed Mar 27 10:49:30 CET 2019


On 24/03/2019 17.39, Sergei Meshveliani wrote:
> I always do so.
> In this my example, M2.agda
> * defines `main' function,
> * is not imported by any module,
> * and I hesitate whether to set the `module' header in M2.agda.
> 
> (the effects are described below).

I suggest that you include the module header in M2.agda as well.

-- 
/NAD


More information about the Agda mailing list