<div dir="ltr"><div>You can find an explanation of grey backgrounds here:</div>    <a href="https://plfa.github.io/Decidable/#logical-connectives">https://plfa.github.io/Decidable/#logical-connectives</a><div>Go well, -- P<br><div></div></div><div><br></div><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, 26 Apr 2020 at 17:37, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.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"><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" target="_blank">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>
</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 href="https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#highlight" target="_blank"><span>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" target="_blank">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>
_______________________________________________<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>