Dot notation for HasEquiv.Equiv?

Stream: lean4

[Michael Stoll]

Can we add HasEquiv.Equiv.symm and HasEquiv.Equiv.trans to enable dot notation like below? It is a bit annoying that I have to write Setoid.symm h instead of h.symm...

def Foo := Nat

def r (x y : Foo) : Prop := sorry

theorem r_refl (x : Foo) : r x x := sorry

theorem r_symm {x y : Foo} (h : r x y) : r y x := sorry

theorem r_trans {x y z : Foo} (h₁ : r x y) (h₂ : r y z) : r x z := sorry

instance : Setoid Foo where
  r := r
  iseqv := {
    refl := r_refl
    symm := r_symm
    trans := r_trans
  }

variable {x y z : Foo} (h : x ≈ y) (h' : y ≈ z)

#check h.symm -- invalid field 'symm', the environment does not contain 'HasEquiv.Equiv.symm'

def HasEquiv.Equiv.symm {α : Type _} [Setoid α] {x y : α} (h : x ≈ y) : y ≈ x :=
  Setoid.symm h

#check h.symm -- OK

#check h.trans h' -- invalid field 'trans', the environment does not contain 'HasEquiv.Equiv.trans'

def HasEquiv.Equiv.trans {α : Type _} [Setoid α] {x y z : α} (h : x ≈ y) (h' : y ≈ z) : x ≈ z :=
  Setoid.trans h h'

#check h.trans h' -- OK

[Eric Wieser]

My impression was that we were moving away from using HasEquiv.Equiv at all in mathlib, and using Setoid.r directly

[Michael Stoll]

Is there notation for docs#Setoid.r (like the one for docs#HasEquiv.Equiv)?

[Eric Wieser]

No, because I think also we're moving (in mathlib) to writing {s : Setoid α} and s.r x y is already very short

[Michael Stoll]

My use case is docs#AbsoluteValue.IsEquiv . How would you spell v ≈ v' where v v' : AbsoluteValue R ℝ?