Skip to main content

export_lean

Function export_lean 

Source
pub fn export_lean(text: &str, file: Option<&str>) -> LeanExportResult
Expand description

Export the supported typed RML fragment to Lean 4 source.