[Agda] A question on a highlighted expression in Emacs

[Apostolis Xekoukoulotakis]

You can read the documentation here :

https://agda.readthedocs.io/en/v2.5.4.2/language/function-definitions.html#case-trees

You shouldn't expand. Check the example in the documentation to learn why
the highlight is important.

On Sat, Mar 2, 2019 at 1:47 AM Jason -Zhong Sheng- Hu <fdhzs2010 at hotmail.com>
wrote:

> Hi,
>
> please consider follow program:
>
>   foo : ℕ → Set
>   foo 0 = {!!}
>   foo a = {!!}
>
> In Emacs, the third line, `foo a`, will be highlighted. I know that I can
> get away with this by expanding `a` to be `suc a`. However, in my real
> project, this expansion corresponds to 5 cases, and their proof body are
> exactly the same.
>
> I understand that this does not introduce any unsoundness, but I want to
> understand what's the reason behind this highlight, and is there any
> programming idiom so that I can get away with this highlight without having
> expand the cases here?
>
>
> *Sincerely Yours, *
>
> * Jason Hu*
> _______________________________________________
> 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/20190302/cfc8c669/attachment.html>