StateRefT

Stream: lean4

[Patrick Massot]

What's the magic with StateRefT? Where is it defined? I cannot jump to its definition and #check StateRefT fails. Is it a keyword?

[Wojciech Nawrocki]

It is basically StateT, except it uses a pointer instead of a product type for efficiency reasons. I think these may be less important these days than they were when StateRefT was introduced.

[Mario Carneiro]

The reason you can't click on StateRefT is because it's actually a macro over StateRefT' which hides an extra type parameter

[Mario Carneiro]

although, last I checked you can click on macros too

[Chris Lovett]

goto ref still doesn't work on StateRefT, I just run into this also, Mario had to point me to the macro. I guess from now on if F12 doesn't find the identifier I have to do a find all for "identifier" to see if it's in a macro. Sometimes that has to be " identifier " because sometimes it's a notation with a space around it...

[Mario Carneiro]

the notations almost never have a space before them, so "identifier works well for me

[Mario Carneiro]

but yes, there is a bug to be tracked down here - go to def should work for macros

[Gabriel Ebner]

I think this is just the standard issue that go-to-definition only works if you import Lean (at least it works for me with that import).