Disable automatic namespace

Stream: lean4

[Martin Dvořák]

Can I disable automatic opening of a namespace for the declaration name prefix?
I would like everything inside a declaration to be evaluated the same way as if it was example instead.

import Mathlib

lemma List.map_comp_comp (l : List ℕ) (f : ℕ → ℤ) (g : ℤ → ℚ) (h : ℚ → ℝ) :
    l.map (h ∘ g ∘ f) = ((l.map f).map g).map h := by
  -- I want `map (g ∘ f) l` to be a syntax error
  have fg : map (g ∘ f) l = (l.map f).map g := by simp
  rw [←fg]
  simp

In the example above, I would like to be forced to write List.map (g ∘ f) l or l.map (g ∘ f) because map (g ∘ f) l would cause a syntax error. Currently map (g ∘ f) l is allowed and I don't like it.

[Damiano Testa]

Is what you are asking to protect the List.map declaration?

[Martin Dvořák]

I would like to have a project-wide setting that makes this behaviour default.

[Kim Morrison]

@Martin Dvořák, I guess this could be turned off, but why do you want this?

[Martin Dvořák]

I want to force myself to write code in a way that will be readable for me later.

[Martin Dvořák]

And also, I don't want to have name changes break the insides.

[Martin Dvořák]

Martin Dvořák said:

I want to force myself to write code in a way that will be readable for me later.

You'll probably say that I should use linters for that, not project settings.

[Damiano Testa]

I find that the automatic open X when the declaration name is X.y is usually very useful, but does create some unpleasant situations. So, having a mechanism to disable the automatic namespacing is something that I would also find useful.

[Martin Dvořák]

I basically never want it; it makes the output of simp? hardly readable for me.

[Martin Dvořák]

RFC: https://github.com/leanprover/lean4/issues/6436

[Eric Wieser]

I don't think "is allowed and I don't like it" is really RFC-appropriate: you should explain what is undesirable about it rather than just stating a personal evaluation.

[Martin Dvořák]

Ultimately, it is all my personal opinion. What is undesirable, however, is that the body of a declaration can change its semantics when the name of the declaration changes (albeit not the main reason why I created the RFC).

[Martin Dvořák]

RFC (second attempt): https://github.com/leanprover/lean4/issues/6855