Enum ProofStateResult 

pub enum ProofStateResult {
    State(Box<ProofStateInfo>),
    Unavailable {
        message: String,
        proof_boundaries: Vec<ProofBoundaryCandidate>,
        proof_boundaries_truncated: bool,
    },
    Ambiguous {
        candidates: Vec<DeclarationTargetInfo>,
    },
    NeedsBuild {
        missing: Vec<String>,
    },
}

Result for ModuleQuerySelector::ProofState.

Variants

State(Box<ProofStateInfo>)

Unavailable

Fields

message: String

proof_boundaries: Vec<ProofBoundaryCandidate>

proof_boundaries_truncated: bool

Ambiguous

Fields

candidates: Vec<DeclarationTargetInfo>

NeedsBuild

Fields

missing: Vec<String>

Trait Implementations

impl Clone for ProofStateResult

fn clone(&self) -> ProofStateResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofStateResult

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

Formats the value using the given formatter.

impl Eq for ProofStateResult

impl PartialEq for ProofStateResult

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for ProofStateResult

impl<'lean> TryFromLean<'lean> for ProofStateResult

fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self>

Decode obj into Self, returning a LeanError::Host with stage [HostStage::Conversion] if the object’s kind or payload is outside the type’s representable range.