pub fn extract_math_module(ctx: &Context) -> Result<String, String>Expand description
Extract every user-defined inductive/definition in ctx into one Rust module —
types, functions, and check_* property fns from proven theorems — WITHOUT a
demo main. This is the linkable artifact bundled into an imperative program’s
mod proven; extract_math_rust wraps it with a self-verifying main for the
standalone Math compile.