Quotient notation on Antisymmetrization

Stream: mathlib4

[Violeta Hernández]

Currently, we can't use quotient notation ⟦x⟧ on the antisymmetrization of a type. Is this intended/fixable?

import Mathlib.Order.Antisymmetrization

def Foo := Antisymmetrization ℕ (· ≤ ·)

-- failed to synthesize
--   LT (Quotient (AntisymmRel.setoid ℕ fun x1 x2 => x1 ≤ x2))
example (x y : ℕ) : (⟦x⟧ : Foo) < ⟦y⟧ ↔ x < y := Iff.rfl

@Yaël Dillies

[Junyan Xu]

I think you need to change docs#Antisymmetrization and Foo to abbrevs. I made docs#DirectLimit an abbrev for this reason.

[Yaël Dillies]

Aren't we moving away from global⟦x⟧ notation? cc @Yuyang Zhao

[Violeta Hernández]

I wasn't aware of that development. In truth this is something we want to do on the game file anyways (where this issue arose) since we'll soon get a second important quotient.