pub fn extract_logic_rust(input: &str) -> Result<String, String>Expand description
Compile a Logic-mode input to runnable Rust.
A ## Theorem: block becomes a model-checker for premises ⊨ goal; a
plain sentence becomes a model-checker for that formula — a self-contained
Model + holds(&Model) -> bool + demo main you can compile and run
(crate::extraction::fol_model). The finite-domain puzzle (Simon grid) is
the exception: it would run the full solver synchronously and freeze the page,
so it bails with a note (use Execute to solve it).