Module proof_convert 

Conversion from parser AST to proof engine representation.

This module bridges the parser’s arena-allocated AST (LogicExpr<'a>) to the proof engine’s owned representation (ProofExpr).

The conversion clones all data into owned Strings, enabling proof trees to persist beyond the arena’s lifetime. Symbols are resolved using the interner at conversion time.

Key Function

logic_expr_to_proof_expr is the main entry point for converting parsed expressions to the format expected by the proof search engine.

Functions

logic_expr_to_proof_expr

Convert a LogicExpr to ProofExpr.

term_to_proof_term

Convert a Term to ProofTerm.