Skip to main content

prove_certify_check_with_defs

logicaffeine_proof::verify

Function prove_certify_check_with_defs 

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

Like prove_certify_check but with user Definitions in scope (Rung 0a).