notation in structures

Stream: general

[Johan Commelin]

Can someone explain me how notation in structures works? Simon changed the definition of a category to:

class category (obj : Type u) : Type (max u (v+1)) :=
(hom      : obj → obj → Type v)
(infixr ` ⟶ `:10 := hom) -- Interesting!
(id       : Π X : obj, X ⟶ X)
(notation `𝟙` := id)
(comp     : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z))
(infixr ` ≫ `:80 := comp)
(id_comp' : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f . obviously)
(comp_id' : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f . obviously)
(assoc'   : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
  (f ≫ g) ≫ h = f ≫ (g ≫ h) . obviously)

But if I #print category, then I don't see this notation being introduced, even though it's still used by the pretty printer.

[Reid Barton]

I assumed the notation commands are still logically independent of the structure, they are just interspersed in the file (so that you can use the notation earlier).

[Sebastian Ullrich]

Local notations (in sections or structures) are gone completely after parsing. Just like tactic blocks are gone after elaboration.

[Johan Commelin]

Ok, so why does the pretty printer use the notation when I ask for #print category? Because the notation was reintroduced afterwards?

[Sebastian Ullrich]

Ah, yes

[Johan Commelin]

Ok, thanks. Everything's cleared up (-;