[Agda] Why the light gray highlighting here?

[Georgi Lyubenov]

Hi!

Related links in the wiki:
https://agda.readthedocs.io/en/v2.6.1.1/tools/emacs-mode.html#highlight
https://agda.readthedocs.io/en/v2.6.1.1/language/function-definitions.html#case-trees

I'm just still not sure what is meant by "hold definitionally" in this
context, seeing as how he is currently defining a function, not trying to
prove anything based on the case tree of some function. Could someone
clarify this?

======
Georgi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200929/bdd74fe2/attachment.html>