[Agda] Light grey background?

[Nils Anders Danielsson]

On 2020-04-26 22:22, Jakob von Raumer wrote:
> what does light grey background shading mean again?

In Emacs you can find out what the highlighting means by using
C-u C-x =. Example:

   open import Agda.Builtin.Bool

   f : Bool → Bool → Bool
   f true  false = false
   f _     true  = true
   f false _     = false

If I place the cursor over the first underscore and type C-u C-x =, then
I get the following output (and more):

   annotation-faces     (agda2-highlight-catchall-clause-face agda2-highlight-symbol-face)

-- 
/NAD