[Agda] Why the light gray highlighting here?

[Thomas Lopatic]

On 2020-09-30 14:31, Nils Anders Danielsson wrote:
> On 2020-09-30 13:41, Thomas Lopatic wrote:
>> What's going on? After all, the second clause says that, by
>> definition, "x xor ⟨⟩" is equal to x. That's definitional equality! Go
>> use it, Agda! Why would you use the first clause's definitional
>> equality for reduction, but not the second clause's?
> 
> Consider the following definition:
> 
>   f : Bool → Bool → Bool
>   f true  _     = true
>   f _     true  = false
>   f false false = false
> 
> Note that the first two clauses disagree on the result for the inputs
> true and true.

Oooooooh! Thank you for that insight.

Thomas