[Agda] Light grey background?

[Andreas Nuyts]

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