## Stream: new members

### Topic: namespace conflict

#### Nicolò Cavalleri (Jul 14 2020 at 10:47):

I am trying to work with continuous bundled functions. I have a problem with namespaces. I defined

structure continuous_map (α : Type*) (β : Type*)
[topological_space α] [topological_space β] :=
(to_fun       : α → β)
(continuous   : continuous to_fun)


However, in the namespace continuous_map continuous conflicts with the already existing continuous. In the algebra section this problem would be solved by renaming continuous to is_continuous. However this is a pretty drastic change. By now I renamed continuous in continuous_map to continuity, but this conflicts with Mathlib naming conventions. Any tip?

#### Mario Carneiro (Jul 14 2020 at 10:49):

I think it's possible to protect definitions after the fact as of some recent version

#### Mario Carneiro (Jul 14 2020 at 10:49):

that way continuous_map.continuous will not compete with continuous even if you open the continuous_map namespace

#### Nicolò Cavalleri (Jul 14 2020 at 10:50):

Mario Carneiro said:

I think it's possible to protect definitions after the fact as of some recent version

How do I do that?

#### Nicolò Cavalleri (Jul 14 2020 at 10:51):

I mean I do not understand "after the fact"

#### Mario Carneiro (Jul 14 2020 at 10:53):

Normally you would protect a definition by writing protected def ... but in this case the definition is the field of a structure, which is automatically generated

#### Mario Carneiro (Jul 14 2020 at 10:54):

so there is no good place to put the word protected

#### Mario Carneiro (Jul 14 2020 at 10:57):

There is possibly a more streamlined version of this, but here's a way to do it

structure foo := (A B : ℕ)

run_cmd tactic.updateex_env $λ e, return$ e.mk_protected foo.B

namespace foo

#check A -- works
#check B -- fails
#check foo.B -- works

end foo


#### Nicolò Cavalleri (Jul 14 2020 at 11:00):

Ok cool this works!!

Thanks!

#### Nicolò Cavalleri (Jul 14 2020 at 11:01):

I guess it is fine if such a line is PRed to Mathlib

#### Sebastien Gouezel (Jul 14 2020 at 11:23):

Even better, you can use @[protect_proj] which is designed precisely for this.

#### Nicolò Cavalleri (Jul 14 2020 at 11:33):

Sebastien Gouezel said:

Even better, you can use @[protect_proj] which is designed precisely for this.

Can I use it to only protect continuous and not to_fun?

#### Rob Lewis (Jul 14 2020 at 11:34):

https://leanprover-community.github.io/mathlib_docs/attributes.html#protect_proj
@[protect_proj without ...] should work.

Ok thanks!

#### Sebastien Gouezel (Jul 14 2020 at 11:45):

Note that protecting to_fun also is probably a good idea, because you will never want to use to_fun directly, but instead you should register a coercion. This would mean that the field continuous should be renamed continuous' or continuous_to_fun in your structure, and the main lemma would be stated as continuity of the coerced function (and you can protect it directly).

#### Reid Barton (Jul 14 2020 at 11:46):

And even if you do use to_fun directly, it would mainly be in the form f.to_fun x

#### Nicolò Cavalleri (Jul 14 2020 at 12:54):

Sebastien Gouezel said:

Note that protecting to_fun also is probably a good idea, because you will never want to use to_fun directly, but instead you should register a coercion. This would mean that the field continuous should be renamed continuous' or continuous_to_fun in your structure, and the main lemma would be stated as continuity of the coerced function (and you can protect it directly).

Why using this trick to protect continuous instead that protect_proj as you suggested before?

#### Reid Barton (Jul 14 2020 at 13:02):

It's not about protecting but rather that, if the primary way to use f as a function is f x and not f.to_fun x, then you want f.continuous to be of the form continuous f and not continuous f.to_fun.

#### Reid Barton (Jul 14 2020 at 13:03):

You cannot define it this way in the structure because the coercion instance does not exist yet.

#### Reid Barton (Jul 14 2020 at 13:04):

But that's fine because dot notation also works with things that are not structure fields.

#### Reid Barton (Jul 14 2020 at 13:04):

This occurs many places in mathlib

#### Nicolò Cavalleri (Jul 14 2020 at 13:23):

Ok thanks

Last updated: May 15 2021 at 00:39 UTC