Zulip Chat Archive

Stream: new members

Topic: why not just open classes


view this post on Zulip Kana (Feb 18 2021 at 18:07):

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

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 18:10):

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

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 18:11):

open is local to the file it is in.

view this post on Zulip kana (Feb 18 2021 at 18:14):

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

view this post on Zulip Eric Wieser (Feb 18 2021 at 18:21):

export perhaps?


Last updated: May 11 2021 at 12:15 UTC