Skip to main content

goal_to_tptp

Function goal_to_tptp 

Source
pub fn goal_to_tptp(goal: &ProofGoal) -> Result<String, Diagnostic>
Expand description

Export a proof goal plus local context as a TPTP FOF problem.