print instances normal_space

Stream: general

[Floris van Doorn]

I think something is messed up in my Lean installation. Does this code snippet work for anyone else?

import topology.separation

#print instances normal_space

[Floris van Doorn]

(I get no output, neither in VSCode, nor on the command line)

[Floris van Doorn]

Oh nvm, nothing to see here. There are just no instances at that point yet.

[Floris van Doorn]

Ok, but there is still something weird going on.

In the following file, I cannot see the output of #print eq in VSCode (I can see it when running from the command line).

import topology.separation
#print instances normal_space
#print eq

Furthermore, if you type

import topology.separation
#print normal_space

and then modify the second line into #print instances normal_space, the messages window doesn't update: it still shows the previous state.

[Kevin Buzzard]

(I can reproduce)