Struct CertificationContext 

pub struct CertificationContext<'a> { /* private fields */ }

Context for certifying derivation trees into kernel terms.

Wraps a kernel [Context] and tracks additional state needed during certification:

• Local variables: Variables bound by lambda abstractions during traversal
• Induction state: For resolving IH (inductive hypothesis) references in step cases

Lifetime

The 'a lifetime ties this context to the kernel context it wraps. The certification context borrows the kernel context immutably.

Example

use logicaffeine_proof::certifier::CertificationContext;
use logicaffeine_kernel::Context;

let kernel_ctx = Context::new();
let cert_ctx = CertificationContext::new(&kernel_ctx);

See Also

• certify - The main function that uses this context
• [Context] - The underlying kernel context

Implementations

impl<'a> CertificationContext<'a>

pub fn new(kernel_ctx: &'a Context) -> Self