pub fn extract_math_rust(ctx: &Context) -> Result<String, String>Expand description
Extract every user-defined inductive and definition in ctx into one Rust
module — the “compile my math to Rust” path for the Math studio. Shared and
StandardLibrary dependencies are pulled in only when a user definition
transitively needs them, and are emitted exactly once.