[Agda] Re: Orange highlights in EMACS Agda mode

[Roly Perera]

Ok, to attempt to answer my own question...looking more carefully at
the annotations I'm guessing it's something to do with termination
checking.  Are there any introductory tutorials on this topic?

2009/11/27 Roly Perera <roly.perera at dynamicaspects.org>:
> Hi,
>
> I've been using Agda for a few weeks but have only recently
> encountered the orange highlighting in the EMACS mode.  I'm remember
> reading about it somewhere but I can't find any mention of it now in
> the documentation, on the Wiki or by searching the mailing list
> archives.
>
> I'm sure it's something basic.  It seems to have arisen since I
> started developing a largish mutually recursive definition in a
> stepwise fashion by introducing postulates for some of the functions
> which will be eventually be defined in the mutual block (not sure if
> that is a legitimate way to proceed anyway, but that's another
> question).  Some things are now highlighted in orange but no actual
> message comes back from the Agda compiler, so I've no idea what it
> means.  Could someone please clarify?
>
> thanks,
> Roly
>