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