[Agda] Why the light gray highlighting here?

[Nils Anders Danielsson]

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.

-- 
/NAD