Enum ModuleQueryBatchResult 

pub enum ModuleQueryBatchResult {
    Diagnostics(LeanElabFailure),
    ProofState(ProofStateResult),
    TypeAt(TypeAtResult),
    References(ReferencesResult),
    DeclarationTarget(DeclarationTargetResult),
    SurroundingDeclaration(SurroundingDeclarationResult),
    DeclarationOutline(DeclarationOutlineResult),
}

Typed payload returned by one successful batch selector.

Variants

Diagnostics(LeanElabFailure)

ProofState(ProofStateResult)

TypeAt(TypeAtResult)

References(ReferencesResult)

DeclarationTarget(DeclarationTargetResult)

SurroundingDeclaration(SurroundingDeclarationResult)

DeclarationOutline(DeclarationOutlineResult)

Trait Implementations

impl Clone for ModuleQueryBatchResult

fn clone(&self) -> ModuleQueryBatchResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ModuleQueryBatchResult

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

Formats the value using the given formatter.

impl<'lean> TryFromLean<'lean> for ModuleQueryBatchResult

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.