logic_expr_to_proof_expr

logicaffeine_language::proof_convert

Function logic_expr_to_proof_expr 

Source 
pub fn logic_expr_to_proof_expr<'a>(
    expr: &LogicExpr<'a>,
    interner: &Interner,
) -> ProofExpr
Expand description

Convert a LogicExpr to ProofExpr.

This is the main entry point for bridging the parser to the proof engine. All Symbols are resolved to owned Strings using the interner.