local open / let open

Stream: lean4

[Jason Gross]

Is there some way to open a namespace locally to a term? None of let open foo;, let open foo in, open foo; seem to work

[Leonardo de Moura]

Jason Gross said:

Is there some way to open a namespace locally to a term? None of let open foo;, let open foo in, open foo; seem to work

I have missed this feature a few times but in tactic mode.
I am going to create an issue for it.