Skip to main content

Module export

lean_ctx::core::context_package

Module export 

Source
Expand description

Export a context package from the current session (#293).

Functionsยง

save_package
Export the current session as a context package (JSON file).