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.