[Agda] Why the light gray highlighting here?
Jason -Zhong Sheng- Hu
fdhzs2010 at hotmail.com
Tue Sep 29 16:12:34 CEST 2020
to expand, "not hold definitionally" means that Agda does not recognize
x xor ⟨⟩ = x
as a definitional equality, as opposed to
⟨⟩ xor y = y
namely, Agda knows ⟨⟩ xor y and y are identical.
The reason is, the function is defined by first doing a case split on x. so the case tree on x is expanded. writing
x xor ⟨⟩ = x
is the same as writing
⟨⟩ xor ⟨⟩ = x
(x O) xor ⟨⟩ = x O
(x I) xor ⟨⟩ = x I
Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Georgi Lyubenov <godzbanebane at gmail.com>
Sent: September 29, 2020 10:08 AM
To: Jason -Zhong Sheng- Hu <fdhzs2010 at hotmail.com>
Cc: David Banas <capn.freako at gmail.com>; Agda mailing list <agda at lists.chalmers.se>
Subject: Re: [Agda] Why the light gray highlighting here?
Hi!
Related links in the wiki:
https://agda.readthedocs.io/en/v2.6.1.1/tools/emacs-mode.html#highlight
https://agda.readthedocs.io/en/v2.6.1.1/language/function-definitions.html#case-trees
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?
======
Georgi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200929/9f199123/attachment.html>
More information about the Agda
mailing list