[Agda] A question on a highlighted expression in Emacs

[Jason -Zhong Sheng- Hu]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190301/54680c00/attachment.html>