pub fn export_lean_bundle_structured(
module_name: &str,
bundle: &ObligationBundle,
) -> LeanExportExpand description
Export a whole bundle as structured Lean module metadata plus source.
pub fn export_lean_bundle_structured(
module_name: &str,
bundle: &ObligationBundle,
) -> LeanExportExport a whole bundle as structured Lean module metadata plus source.