[Agda] Expanding literate Agda

[Ulf Norell]

I'm also in favour of the first solution. Using double extensions is not
really standard practice and might confuse both users and tools. Also, it
sounds like inferring the format won't be that hard.

/ Ulf

On Sun, Oct 12, 2014 at 11:51 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
wrote:

>
> On 12 October 2014 06:28, Pepijn Kokke <pepijn.kokke at gmail.com> wrote:
>
>> Try to infer the literate format from the file, making it explicit with
>> Agda command-line arguments if necessary.
>
>
> +1
>
>
> --
> Andrés
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141013/d97f1afb/attachment.html