namespace in metaprogramming

Stream: Is there code for X?

[Huajian Xin]

The standard method set_env (environment) in tactic.lean seems to be equivalent to the open (environment) in text editor, but if there is any method equivalent to the direct namespace (environment) and end (environment) in metaprogramming?
The specific problem is that, when I run some specific tactic, e.g. unfold read, after the open (environment) command I must use unfold buffer.read while when the hole theorem block live in the namespace block I just need to use unfold read. Is there any metaprogramming method corrosponding to this style?
The original input-output in lean-gym environment of this example:

["init_search",["buffer.read_eq_read'","buffer"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"⊢ ∀ {α : Type u} [_inst_1 : inhabited α] (b : buffer α) (i : ℕ) (h : i < b.size), b.read ⟨i, h⟩ = b.read' i","tactic_state_id":"0"}
["run_tac",["0","0","try{intros}"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"α : Type u,_inst_1 : inhabited α,b : buffer α,i : ℕ,h : i < b.size⊢ b.read ⟨i, h⟩ = b.read' i","tactic_state_id":"1"}
["run_tac",["0","1","cases b"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"α : Type u,_inst_1 : inhabited α,i b_fst : ℕ,b_snd : array b_fst α,h : i < size ⟨b_fst, b_snd⟩⊢ read ⟨b_fst, b_snd⟩ ⟨i, h⟩ = read' ⟨b_fst, b_snd⟩ i","tactic_state_id":"2"}
["run_tac",["0","2","unfold read read'"]]
{"error":"gen_tac_and_capture_res_failed: pos=(some ⟨1, 2⟩) msg=unfold tactic failed, read does not have equational lemmas nor is a projection","proof_steps":[],"search_id":null,"tactic_state":null,"tactic_state_id":null}
["run_tac",["0","2","unfold buffer.read buffer.read'"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"α : Type u,_inst_1 : inhabited α,i b_fst : ℕ,b_snd : array b_fst α,h : i < size ⟨b_fst, b_snd⟩ \n⊢ b_snd.read ⟨i, h⟩ = b_snd.read' i","tactic_state_id":"3"}

[Floris van Doorn]

docs#tactic.set_env is very different from the open command, and should almost be never be used when metaprogramming.

[Floris van Doorn]

Note: there is docs#environment.execute_open

[Floris van Doorn]

As far as I can see there is no way to "inject" namespace buffer into a tactic.
Note: the reason that unfold read fails is that read is overloaded with monad_reader.read.

[Huajian Xin]

Thanks! And I wonder that how can I force the interpreter consider read as buffer.read instead of (or before as)monad_reader.read? Is there any way to command that?