No `⟦x⟧` notation in infoview?

Stream: mathlib4

[Kevin Buzzard]

import Mathlib.Data.Quot -- ⟦_⟧ notation

instance X.setoid : Setoid Nat where
  r := (. = .)
  iseqv := sorry

abbrev Q := Quotient X.setoid

example (x : Nat) : (⟦x⟧ : Q) = ⟦x⟧ := by
  /-
  x : Nat
  ⊢ Quotient.mk X.setoid x = Quotient.mk X.setoid x
  -/
  sorry

I was expecting to see ⟦x⟧ = ⟦x⟧. How do I get quotient notation in the infoview? I can't even seem to rewrite to the quotient notation.

[Eric Wieser]

I suspect there is no delaborator for it

[Kevin Buzzard]

@Kyle Miller do you know how to fix this?

[Kyle Miller]

#8022 Often it seems that when a notation doesn't pretty print you can turn it into a notation3, which has a more sophisticated delaborator generator.

[Eric Wieser]

My understanding is that notation3 was only intended as a crutch for porting. It sounds like this is not the case, and so we should either:

• Just rename it, if no part of the tactic is a porting crutch
• Split the tactic into a notation_with_delab (with no hacks) and notation3 (which is notation_with_delab + compatibility hacks), and slowly eradicate the latter

[Kyle Miller]

notation3 tries to do everything that the Lean 3 version did, and I think in principle it doesn't have any features we don't want. Renaming it seems sensible to me.

[Kyle Miller]

I hope eventually notation itself becomes better at generating delaborators.

The main interesting feature of notation3 is that it has some scoping constructs for dealing with nested binders.