## Stream: lean4

### Topic: local open / let open

#### Jason Gross (Mar 05 2021 at 18:38):

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 (Mar 05 2021 at 18:42):

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.

Last updated: May 07 2021 at 11:09 UTC