pub fn goal_to_tptp(goal: &ProofGoal) -> Result<String, Diagnostic>Expand description
Export a proof goal plus local context as a TPTP FOF problem.
pub fn goal_to_tptp(goal: &ProofGoal) -> Result<String, Diagnostic>Export a proof goal plus local context as a TPTP FOF problem.