<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);">
to expand, "not hold definitionally" means that Agda does not recognize<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<font face="monospace"><span style="background-color: rgb(238, 238, 238);">x xor ⟨⟩</span> = x</font></div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
as a definitional equality, as opposed to <br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<font face="monospace">⟨⟩ xor y = y</font><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
namely, Agda knows<font face="monospace"> ⟨⟩ xor y and y</font> are identical.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
The reason is, the function is defined by first doing a case split on <code>x</code>. so the case tree on
<code>x</code> is expanded. writing</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<font face="monospace"><span style="background-color: rgb(238, 238, 238);">x xor ⟨⟩</span> = x</font></div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
is the same as writing</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<font face="monospace"><span style="background-color: rgb(238, 238, 238);"><font face="monospace"><span style="background-color: rgb(238, 238, 238);">⟨⟩</span></font> xor ⟨⟩</span> = x</font><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<font face="monospace"><span style="background-color: rgb(238, 238, 238);"><font face="monospace"><span style="background-color: rgb(238, 238, 238);"></span></font><font face="monospace">(x O)</font> xor ⟨⟩</span> = <font face="monospace"><span style="background-color: rgb(238, 238, 238);"><font face="monospace">x
O</font></span></font></font><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<font face="monospace"><span style="background-color: rgb(238, 238, 238);"><font face="monospace">(x I)</font> xor ⟨⟩</span> = x I</font><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> Georgi Lyubenov <godzbanebane@gmail.com><br>
<b>Sent:</b> September 29, 2020 10:08 AM<br>
<b>To:</b> Jason -Zhong Sheng- Hu <fdhzs2010@hotmail.com><br>
<b>Cc:</b> David Banas <capn.freako@gmail.com>; Agda mailing list <agda@lists.chalmers.se><br>
<b>Subject:</b> Re: [Agda] Why the light gray highlighting here?</font>
<div> </div>
</div>
<div>
<div dir="ltr">Hi!<br>
<br>
Related links in the wiki:<br>
<a href="https://agda.readthedocs.io/en/v2.6.1.1/tools/emacs-mode.html#highlight">https://agda.readthedocs.io/en/v2.6.1.1/tools/emacs-mode.html#highlight</a><br>
<a href="https://agda.readthedocs.io/en/v2.6.1.1/language/function-definitions.html#case-trees">https://agda.readthedocs.io/en/v2.6.1.1/language/function-definitions.html#case-trees</a><br>
<br>
I'm just still not sure what is meant by "hold definitionally" in this context, seeing as how he is currently defining a function, not trying to prove anything based on the case tree of some function. Could someone clarify this?<br>
<br>
======<br>
Georgi</div>
</div>
</body>
</html>