Zulip Chat Archive

Stream: lean4

Topic: Serialisation to oleans

Jannis Limperg (Jun 22 2021 at 12:28):

I found a note somewhere in the source code that serialisation to oleans (as used by PersistentEnvExtension) doesn't support closures. Is this still accurate? Any other limitations I should be aware of?

Sebastian Ullrich (Jun 22 2021 at 13:28):

Closures and external objects (which you are unlikely to use) should be the only ones

Jannis Limperg (Jun 22 2021 at 14:17):

Nice, I can work with that. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC