[Agda] Light grey background?

[Jesper Cockx]

Hi Jakob and Andreas,

It is explained in the page on function definitions, specifically in the
section on case trees (
https://agda.readthedocs.io/en/v2.6.1/language/function-definitions.html#case-trees
):

> 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 highlighted
> <https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#highlight>
> by Emacs.
>
-- Jesper

On Sun, Apr 26, 2020 at 10:35 PM Andreas Nuyts <andreas.nuyts at kuleuven.be>
wrote:

> Dear Jakob,
>
> I would refer you to the agda docs,
> https://agda.readthedocs.io
> but surprisingly these have no entry on pattern matching.
> While we're waiting for someone to give a more thorough answer: a case
> in a pattern matching definition gets a light grey background when it
> doesn't hold as a definitional equation, typically because it is a
> fallthrough case and further matching of the arguments is necessary to
> establish that none of the prior cases apply.
>
> Best,
> Andreas
>
> On 26/04/2020 22:22, Jakob von Raumer wrote:
> > Hi all,
> >
> > what does light grey background shading mean again? It's a bit awkward
> > to have to be googline something like this...
> >
> > Cheers
> >
> > Jakob
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200426/0cbb66d9/attachment.html>