Skip to main content

generate_rust_code

Function generate_rust_code 

Source
pub fn generate_rust_code(source: &str) -> Result<String, ParseError>
Expand description

Generate Rust code from LOGOS source — the Studio Code path. Mixed-document aware: a source interleaving imperative code with Coq-style math (Definition/## Theorem:/…) extracts the math into a bundled mod proven that the imperative half calls into. Pure imperative source is a no-op partition.