colour of `abbrev`

Stream: Zulip meta

[Kevin Buzzard]

On Zulip, abbrev (at the beginning of a line near the bottom of this code) is showing up in a different colour to everything around it (as is import, but at least import is some non-default colour). Is this expected?

import Mathlib.Data.Nat.Basic

def is_filter (F : Nat → Nat ): Prop := sorry

def filter_example : Nat → Nat := sorry

theorem foo : is_filter filter_example := sorry

class Filter (filter: Nat → Nat) : Prop where
  filter_proof: is_filter filter

instance : Filter (filter_example) := ⟨foo⟩

def refine (N: Nat) (fil: Nat → Nat) : Nat → Nat := sorry

theorem refined_filter_is_filter (N: Nat) (fil: Nat → Nat) [inst: Filter fil] : is_filter (refine N fil) := sorry

instance (N : Nat) (fil: Nat → Nat) [Filter fil] : Filter (refine N fil) := ⟨refined_filter_is_filter N fil⟩

abbrev refined_filter_example := refine Nat.zero filter_example

theorem test1 : is_filter refined_filter_example := by apply refined_filter_is_filter

theorem test2 : Filter refined_filter_example := inferInstance

[Alex Vandiver]

I believe that @Eric Wieser recently updated the Pygments parser for lean; I don't know if we've taken that update yet, or if this is a change from that.

[Eric Wieser]

Pygments has not yet made a release with that update

[Eric Wieser]

But the update will fix the issue above (after we also reconfigure our default language on Zulip to be Lean4)

[Eric Wieser]

GitHub claims they're aiming for a release in the next few days