Struct LeanWorkerDeclarationVerificationFacts 

pub struct LeanWorkerDeclarationVerificationFacts {
    pub target: Option<LeanWorkerDeclarationTargetInfo>,
    pub diagnostics: LeanWorkerElabFailure,
    pub unresolved_goals: Vec<LeanWorkerRenderedInfo>,
    pub contains_sorry: bool,
    pub contains_admit: bool,
    pub contains_sorry_ax: bool,
    pub axioms: Vec<String>,
    pub axioms_truncated: bool,
    pub output_truncated: bool,
    pub candidates: Vec<LeanWorkerDeclarationTargetInfo>,
    pub axioms_available: bool,
}

Bounded facts returned by declaration verification.

Fields

target: Option<LeanWorkerDeclarationTargetInfo>

diagnostics: LeanWorkerElabFailure

unresolved_goals: Vec<LeanWorkerRenderedInfo>

contains_sorry: bool

contains_admit: bool

contains_sorry_ax: bool

axioms: Vec<String>

axioms_truncated: bool

output_truncated: bool

candidates: Vec<LeanWorkerDeclarationTargetInfo>

Competing declarations when verification_status is Ambiguous; empty otherwise.

axioms_available: bool

false when the axiom dependency set could not be computed (the target did not resolve, or the walk was not requested): an empty axioms then means “not computed”, not “no axioms”. true with empty axioms is a genuine no-nontrivial-axioms result.

Implementations

impl LeanWorkerDeclarationVerificationFacts

pub fn unavailable() -> LeanWorkerDeclarationVerificationFacts

Facts for a verdict the worker could not substantiate — for example when the child aborted mid-job and the supervisor synthesised a degraded verdict. Every field is empty and axioms_available is false, so the axiom set reads as “not computed” rather than “no axioms”.

Trait Implementations

impl Clone for LeanWorkerDeclarationVerificationFacts

fn clone(&self) -> LeanWorkerDeclarationVerificationFacts

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LeanWorkerDeclarationVerificationFacts

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for LeanWorkerDeclarationVerificationFacts

fn deserialize<__D>( __deserializer: __D, ) -> Result<LeanWorkerDeclarationVerificationFacts, <__D as Deserializer<'de>>::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for LeanWorkerDeclarationVerificationFacts

impl PartialEq for LeanWorkerDeclarationVerificationFacts

fn eq(&self, other: &LeanWorkerDeclarationVerificationFacts) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for LeanWorkerDeclarationVerificationFacts

fn serialize<__S>( &self, __serializer: __S, ) -> Result<<__S as Serializer>::Ok, <__S as Serializer>::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for LeanWorkerDeclarationVerificationFacts