why not just open classes

Stream: new members

[Kana]

Why in stdlib a lot of custom selector functions from classes instead of just openings of them?

class has_to_string (α : Type u) :=
(to_string : α → string)

def to_string {α : Type u} [has_to_string α] : α → string :=
has_to_string.to_string

instead of

class has_to_string (α : Type u) :=
(to_string : α → string)
open has_to_string

[Yakov Pechersky]

So that to_string is available everywhere without having to do open has_to_string in your file.

[Yakov Pechersky]

open is local to the file it is in.

[kana]

I understood, thanks. Are there any ways to include content of one namespace into current?

[Eric Wieser]

export perhaps?