[Agda] A question on a highlighted expression in Emacs

[Jason -Zhong Sheng- Hu]

i see. thank you. so it's a highlight that signifies the particular line is not definitionally convertible.

Sincerely Yours,

Jason Hu
________________________________
From: Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis at gmail.com>
Sent: March 1, 2019 7:12 PM
To: Jason -Zhong Sheng- Hu
Cc: agda at lists.chalmers.se
Subject: Re: [Agda] A question on a highlighted expression in Emacs

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<mailto: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<mailto: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/2bcff644/attachment.html>