[Agda] Why the light gray highlighting here?

[Philip Wadler]

See:
    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 Tue, 29 Sep 2020 at 15:01, David Banas <capn.freako at gmail.com> wrote:

> Hi all,
>
> I'm wondering why the second line in my definition for `*xor*` below is
> being partially highlighted in a very light gray background, as shown.
>
> Thanks,
> -db
>
> data Bin : Set where
>   ⟨⟩ : Bin
>   _O : Bin → Bin
>   _I : Bin → Bin
>
> _xor_ : Bin → Bin → Bin
> ⟨⟩    xor y      =  y
> x     xor ⟨⟩     =  x
> (x O) xor (y O)  = (x xor y) O
> (x O) xor (y I)  = (x xor y) I
> (x I) xor (y O)  = (x xor y) I
> (x I) xor (y I)  = (x xor y) O
>
> _______________________________________________
> 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/20200929/89b1630c/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200929/89b1630c/attachment.ksh>