pub fn parse_theorem(input: &str) -> Result<Command, ParseError>Expand description
Parse “## Theorem: [name] Statement: [proposition].” into Command::Definition
This is for theorem declarations like:
## Theorem: Godel_First_Incompleteness\n Statement: Consistent implies Not(Provable(G)).