RFC: optionally disable automatic namespace

[madvorak]

I would like to have a project-wide setting to disable automatic opening of a namespace for the declaration's name prefix.
I would like everything inside a declaration to be evaluated the same way as if it was example instead.

theorem List.map_comp_comp {α β γ δ : Type}
    (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, with the new settings, I would 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.

Discussion:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Disable.20automatic.20namespace