<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
because this line does not hold definitionally and you have to prove it. this is just a reminder. this definition itself isn't doing anything wrong.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div>
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color: rgb(69, 129, 142);"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>
</div>
</div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of David Banas <capn.freako@gmail.com><br>
<b>Sent:</b> September 29, 2020 10:01 AM<br>
<b>To:</b> Agda mailing list <agda@lists.chalmers.se><br>
<b>Subject:</b> [Agda] Why the light gray highlighting here?</font>
<div> </div>
</div>
<div>
<div dir="ltr">Hi all,<br>
<div><br>
</div>
<div>I'm wondering why the second line in my definition for `<font face="monospace"><b>xor</b></font>` below is being partially highlighted in a very light gray background, as shown.</div>
<div><br>
</div>
<div>Thanks,</div>
<div>-db</div>
<div><br>
</div>
<div><font face="monospace">data Bin : Set where<br>
⟨⟩ : Bin<br>
_O : Bin → Bin<br>
_I : Bin → Bin<br>
</font></div>
<div><font face="monospace"><br>
</font></div>
<div><font face="monospace">_xor_ : Bin → Bin → Bin<br>
⟨⟩ xor y = y<br>
<span style="background-color:rgb(238,238,238)">x xor ⟨⟩</span> = x<br>
(x O) xor (y O) = (x xor y) O<br>
(x O) xor (y I) = (x xor y) I<br>
(x I) xor (y O) = (x xor y) I<br>
(x I) xor (y I) = (x xor y) O<br>
</font></div>
<div><br>
</div>
</div>
</div>
</body>
</html>