Exporting scoped notation between namespaces

Stream: new members

[Jad Ghalayini]

Say I define a notation in some namespace, e.g.

namespace Hello

scoped infixl:81 " ⋉ " => bleh

end Hello

Is there an idiomatic way to re-export this to another namespace, e.g.

namespace Hello2

(somehow import ⋉)

end Hello2

such that there won't be a conflict if both namespaces are open?

[Aaron Liu]

Do you want something like open scoped Hello?

[Jad Ghalayini]

Will that work if I import Hello2?

[Jad Ghalayini]

What I'd like is to be able to do

open Hello2

(use ⋉ without knowing Hello exists)

[Nick Ward]

You could use scoped[Hello2] notation to put the notation into a namespace different from where it is defined.

[Nick Ward]

So if you did scoped[Shared] notation .. then both Hello and Hello2 could open scoped Shared.

[Jad Ghalayini]

Ah, let me try it...

[Jad Ghalayini]

Hmm... can we avoid that? I don't want to complicate the API, since most people will only ever use Hello2 (not Hello or Shared)?

[Nick Ward]

You could put it directly into Hello2 with scoped[Hello2] notation from Hello.

[Nick Ward]

(it's also possible re-exporting is a thing and I've just never stumbled across it).

[Yaël Dillies]

Do you know about export?

[Jad Ghalayini]

Yes, but that's for names right

[Jad Ghalayini]

Like

export PremonoidalCategory (ltimes rtimes Pentagon)

[Jad Ghalayini]

What I'm experimenting with is moving

/-- Notation for the monoidal `associator`: `(X ⊗ Y) ⊗ Z ≃ X ⊗ (Y ⊗ Z)` -/
scoped notation "α_" => MonoidalCategoryStruct.associator

/-- Notation for the `leftUnitor`: `𝟙_C ⊗ X ≃ X` -/
scoped notation "λ_" => MonoidalCategoryStruct.leftUnitor

/-- Notation for the `rightUnitor`: `X ⊗ 𝟙_C ≃ X` -/
scoped notation "ρ_" => MonoidalCategoryStruct.rightUnitor

to PremonoidalCategory and somehow re-exporting it

[Nick Ward]

I did not! Maybe the following would work?

namespace Foo
def add1 (n : ℕ) := n + 1
notation (name := note) "~" n "~" => add1 n
end Foo

namespace Bar
export Foo (note)
end Bar

[Yaël Dillies]

Yes, exactly, notations too have names, so I would hope they can be similarly exported (I have no clue whether they actually can)

[Jad Ghalayini]

Nope I get unknown constant 'CategoryTheory.MonoidalCategoryStruct.tensorObjNotation'

[Jad Ghalayini]

Sorry, had a typo, now I get invalid 'export', self export

[Jad Ghalayini]

No wait it works

[Jad Ghalayini]

I am very sleep deprived, ignore that

[Nick Ward]

Not sure if the above actually worked or not, but the better solution might be a "neutral" namespace, where you define all of the notation (whether in PremonoidalCategory or MonoidalCategory) as scoped[Monoidal] notation, then everyone just does open scoped Monoidal instead of open scoped MonoidalCategory.

[Jad Ghalayini]

So it works but then other things in other files broke in subtle ways, so I decided to just leave it for now