[Agda-dev] Agda Compiler Alterations Guide :: Notes

[Nils Anders Danielsson]

On 2018-10-02 15:15, Musa Al-hassy wrote:
> In particular, to make an observable change I wanted the compiler
> to accept the keyword `mmodule` in place of the existing `module` keyword.

I don't think you need to modify the parser. However, it might make
sense to modify Agda.Syntax.Concrete.Pretty.

> My steps and code can be found at https://github.com/alhassy/agda

Agda complains because you did not replace module with mmodule in
Agda.Primitive (see src/data/lib/prim/Agda/Primitive.agda). This module
is loaded automatically by Agda.

-- 
/NAD