Skip to main content

check_derivation_with_defs

logicaffeine_proof::verify

Function check_derivation_with_defs 

Source 
pub fn check_derivation_with_defs(
    premises: &[ProofExpr],
    goal: &ProofExpr,
    definitions: &[Definition],
    derivation: DerivationTree,
) -> VerifiedProof
Expand description

Like check_derivation but with user Definitions in scope (Rung 0a), so an externally-built derivation of a definiens can certify against a goal stated with the definiendum — δ reconciles them at the root.