<div dir="ltr">Hi!<br><br>Related links in the wiki:<br><a href="https://agda.readthedocs.io/en/v2.6.1.1/tools/emacs-mode.html#highlight">https://agda.readthedocs.io/en/v2.6.1.1/tools/emacs-mode.html#highlight</a><br><a href="https://agda.readthedocs.io/en/v2.6.1.1/language/function-definitions.html#case-trees">https://agda.readthedocs.io/en/v2.6.1.1/language/function-definitions.html#case-trees</a><br><br>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?<br><br>======<br>Georgi</div>