[Agda] Why the light gray highlighting here?
Jason -Zhong Sheng- Hu
fdhzs2010 at hotmail.com
Tue Sep 29 16:04:14 CEST 2020
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.
Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of David Banas <capn.freako at gmail.com>
Sent: September 29, 2020 10:01 AM
To: Agda mailing list <agda at lists.chalmers.se>
Subject: [Agda] Why the light gray highlighting here?
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200929/bb3e7cd2/attachment.html>
More information about the Agda
mailing list