[Agda] .lagda.md in emacs interactive mode

[Pierre-Evariste Dagand]

> On 11/03/2019 13.39, Martin Escardo wrote:
> > When I start emacs with such a file, it doesn't start with the agda
> > mode. Do I need to add something to my .emacs?
>
> The Emacs mode currently does not support .lagda.md files:
>
>    https://github.com/agda/agda/issues/2837

But that shouldn't stop you from trying: here is a .dir-locals

https://github.com/pedagand/MPRI-2.4-DTP/blob/master/.dir-locals.el

to put at the root at your project. Then, Emacs will let you load,
edit, etc. your literate files.

For instance, this example (and all the others in that repos)

https://github.com/pedagand/MPRI-2.4-DTP/blob/master/01-effectful/Monad.lagda.rst

works like a charm (I use 'rst' files, YMMV with markdown).


Use at your own risk,

-- 
Pierre-Evariste