Zulip Chat Archive

Stream: lean4

Topic: local open / let open


view this post on Zulip 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

view this post on Zulip 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