opening twice

Stream: general

[Kevin Buzzard]

open set

def set.F : ℤ → ℤ := id

-- example : F = F := rfl
-- unknown identifier 'F'

open set -- again!

example : F = F := rfl

I hadn't noticed this before. Does open set go through all things called set.X and say "OK so you can just call this X"? If I add a new thing in the set namespace then I seem to have to open again to get access to it?

[Gabriel Ebner]

Yes.

[Kevin Buzzard]

So open can be quite costly!

[Yury G. Kudryashov]

AFAIR, some slides said that this is going to be fixed in Lean 4.