[Agda] Light grey background?

[Philip Wadler]

You can find an explanation of grey backgrounds here:
    https://plfa.github.io/Decidable/#logical-connectives
Go well, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/



On Sun, 26 Apr 2020 at 17:37, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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
>>
> _______________________________________________
> 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/31fb8f39/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200426/31fb8f39/attachment.ksh>