Enum ModuleQuerySelector 

pub enum ModuleQuerySelector {
    Diagnostics {
        id: String,
    },
    ProofState {
        id: String,
        line: u32,
        column: u32,
    },
    ProofStateInDeclaration {
        id: String,
        declaration: String,
        position: ProofPositionSelector,
        locals_raw: bool,
    },
    TypeAt {
        id: String,
        line: u32,
        column: u32,
    },
    References {
        id: String,
        name: String,
    },
    DeclarationTarget {
        id: String,
        name: Option<String>,
        line: Option<u32>,
        column: Option<u32>,
    },
    SurroundingDeclaration {
        id: String,
        line: u32,
        column: u32,
    },
    DeclarationOutline {
        id: String,
    },
}

One selector inside a batched module-processing request.

Variants

Diagnostics

Fields

id: String

ProofState

Fields

id: String

line: u32

column: u32

ProofStateInDeclaration

Fields

id: String

declaration: String

position: ProofPositionSelector

locals_raw: bool

Render local hypotheses as raw, fully-elaborated Expr text rather than the default notation-aware delaboration. Expert opt-out.

TypeAt

Fields

id: String

line: u32

column: u32

References

Fields

id: String

name: String

DeclarationTarget

Fields

id: String

name: Option<String>

line: Option<u32>

column: Option<u32>

SurroundingDeclaration

Fields

id: String

line: u32

column: u32

DeclarationOutline

Fields

id: String

Implementations

impl ModuleQuerySelector

pub fn id(&self) -> &str

Trait Implementations

impl Clone for ModuleQuerySelector

fn clone(&self) -> ModuleQuerySelector

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ModuleQuerySelector

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

Formats the value using the given formatter.

impl Eq for ModuleQuerySelector

impl<'lean> IntoLean<'lean> for ModuleQuerySelector

fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean>

Allocate (or scalar-box) a Lean representation of self and return the owned handle.

impl<'lean> LeanAbi<'lean> for ModuleQuerySelector

type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr

The C-ABI type Lake emits for this Lean type at function signatures.

impl PartialEq for ModuleQuerySelector

fn eq(&self, other: &ModuleQuerySelector) -> 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 SealedAbi for ModuleQuerySelector

impl StructuralPartialEq for ModuleQuerySelector

impl<'lean> TryFromLean<'lean> for ModuleQuerySelector

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.