does pickling preserve sharing

Stream: lean4

[Joachim Breitner]

I strongly assume the answer is yes, but just checking: Does pickling heap data structures to disk preserve sharing? I.e. if I place the same Lean.Name into various data structures, will they be stored only once?

[Sebastian Ullrich]

Not only does it preserve sharing, it implements maximum sharing (by comparing objects on the byte level)

[Joachim Breitner]

Neat!