ext attribute on a class?

Stream: general

[Thomas Murrills]

What does it mean when a class, in particular docs#has_le in mathlib3, is tagged with @[ext]? I’m struggling to see how or when this would be applied as an extensionality lemma…