<div dir="ltr"><div>Hi Jakob and Andreas,</div><div><br></div><div>It is explained in the page on function definitions, specifically in the section on case trees (<a href="https://agda.readthedocs.io/en/v2.6.1/language/function-definitions.html#case-trees">https://agda.readthedocs.io/en/v2.6.1/language/function-definitions.html#case-trees</a>):</div><div></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div class="gmail-highlight-agda gmail-notranslate">
</div>
<p>Clauses which do not hold definitionally are usually (but not always)
the result of writing clauses by hand instead of using Agda’s case
split tactic. These clauses are <a class="gmail-reference gmail-internal" href="https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#highlight"><span class="gmail-std gmail-std-ref">highlighted</span></a> by
Emacs.</p></div></blockquote><div></div><div>-- Jesper <br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Apr 26, 2020 at 10:35 PM Andreas Nuyts <<a href="mailto:andreas.nuyts@kuleuven.be">andreas.nuyts@kuleuven.be</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear Jakob,<br>
<br>
I would refer you to the agda docs,<br>
<a href="https://agda.readthedocs.io" rel="noreferrer" target="_blank">https://agda.readthedocs.io</a><br>
but surprisingly these have no entry on pattern matching.<br>
While we're waiting for someone to give a more thorough answer: a case <br>
in a pattern matching definition gets a light grey background when it <br>
doesn't hold as a definitional equation, typically because it is a <br>
fallthrough case and further matching of the arguments is necessary to <br>
establish that none of the prior cases apply.<br>
<br>
Best,<br>
Andreas<br>
<br>
On 26/04/2020 22:22, Jakob von Raumer wrote:<br>
> Hi all,<br>
><br>
> what does light grey background shading mean again? It's a bit awkward<br>
> to have to be googline something like this...<br>
><br>
> Cheers<br>
><br>
> Jakob<br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>