Struct ProofAttemptEnvelope 

pub struct ProofAttemptEnvelope {
    pub candidates: Vec<ProofAttemptRow>,
    pub candidate_limit: u32,
    pub candidates_truncated: bool,
    pub entry_goals: Vec<RenderedInfo>,
    pub locals: Vec<LocalInfo>,
}

Envelope for a bounded proof attempt.

Fields

candidates: Vec<ProofAttemptRow>

candidate_limit: u32

candidates_truncated: bool

entry_goals: Vec<RenderedInfo>

Goal state at the resolved proof position before any candidate ran — the selected tactic’s goals_before, identical to what the proof-position query reports as goals_before at the same position, rendered once per batch by the shim. Empty when the entry state is degraded or unresolvable (resolution failure or the source-text fallback).

locals: Vec<LocalInfo>

Local hypotheses at the resolved proof position, rendered once per batch with the proof-position query’s pretty locals mode from the same goals_before state — identical to what the proof-position query reports as locals at the same position. Empty under the same conditions as entry_goals.

Trait Implementations

impl Clone for ProofAttemptEnvelope

fn clone(&self) -> ProofAttemptEnvelope

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofAttemptEnvelope

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

Formats the value using the given formatter.

impl<'lean> TryFromLean<'lean> for ProofAttemptEnvelope

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.