pub fn implicit_main(source: &str) -> Option<String>Expand description
Partition a possibly-MIXED document into its imperative and math streams.
A mixed document interleaves imperative LOGOS (## To/## Main/statements) with
Coq-style math (Definition/Inductive/Axiom/Theorem/Lemma/Fixpoint) and
literate ## Theorem:/## Lemma: blocks. The math blocks feed the Forge (extracted
into mod proven); the imperative blocks compile normally and call into it.
Returns (imperative_src, Some(math_src)) when math is present, or
(source.to_string(), None) for a pure imperative program — so that path is a
guaranteed no-op (byte-identical compile). In imperative_src the math lines are
BLANKED (kept as empty lines), not deleted, so imperative line numbers — and thus
error spans — stay aligned with the original source.
## To/## A X is one of stay imperative (only the Coq keywords and ## Theorem:/
## Lemma: route to math), so this never steals an imperative function or enum.
IMPLICIT MAIN: a source with no ## headers whose first non-blank line
reads as an imperative statement runs as its own ## Main body — a bare
script no longer parses as logic prose and runs to empty output.
Natural-language documents (no statement-keyword opening) are untouched.
Returns the wrapped source, or None when the input is not a bare script.