What does Void do?

Stream: lean4

[Luke West]

What does the Void type do in lean4/src/Init/System/ST.lean? How should I think about it? I've been looking through those files to get a better idea of how the IO monad actually works, but Void is opaque and doesn't have any documentation that I can see.

[Henrik Böving]

It's a piece of data that gets erased in the last third of the compiler pipeline. This allows ST and BaseIO to have allocation free return values because they don't need to return a pair of RealWorld and the data anymore but just the data