pub struct VerifiedProof {
pub derivation: Option<DerivationTree>,
pub proof_term: Option<Term>,
pub kernel_ctx: Context,
pub verified: bool,
pub verification_error: Option<String>,
}Expand description
Outcome of running a goal through prove → certify → kernel type-check.
The invariant: verified == true iff proof_term.is_some() and that
term type-checks in kernel_ctx. When verification fails, derivation may
still be present (the chainer found a derivation) but it is never reported
as verified — verification_error explains where the chain broke.
Fields§
§derivation: Option<DerivationTree>The derivation found by backward chaining, if any.
proof_term: Option<Term>The certified kernel proof term, present only when verified.
kernel_ctx: ContextThe kernel context the proof term was checked in (predicates, constants, and premise hypotheses registered).
verified: boolTrue iff a proof term was certified and kernel type-checked.
verification_error: Option<String>Where the chain broke (search, certification, or type-check), if it did.
Auto Trait Implementations§
impl Freeze for VerifiedProof
impl RefUnwindSafe for VerifiedProof
impl Send for VerifiedProof
impl Sync for VerifiedProof
impl Unpin for VerifiedProof
impl UnsafeUnpin for VerifiedProof
impl UnwindSafe for VerifiedProof
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more