Struct Correspondence 

pub struct Correspondence {
    pub lean: String,
    pub importer_key: String,
    pub logos: String,
    pub kind: DeclarationKind,
    pub origin: Origin,
    pub form: Form,
    pub levels: Vec<(String, String)>,
    pub lines: Option<(usize, usize)>,
}

One Lean declaration and the LOGOS declaration that carries it.

Fields

lean: String

The Lean name as Lean writes it; for a reader-introduced helper, the importer’s own name; empty for a constant the fresh LOGOS context derives itself (origin Synthesized), which Lean never had.

importer_key: String

The key the importer registered the declaration under; empty for a derived constant.

logos: String

The absolute LOGOS name.

kind: DeclarationKind

origin: Origin

form: Form

levels: Vec<(String, String)>

Universe parameters, in order: (importer’s name, LOGOS name).

lines: Option<(usize, usize)>

The 1-based, inclusive line range of the LOGOS declaration in the document. None for a prelude identity, which is not written. The Lean side carries no span: an export records no source positions.

Trait Implementations

impl Clone for Correspondence

fn clone(&self) -> Correspondence

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Correspondence

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

Formats the value using the given formatter.

impl PartialEq for Correspondence

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

impl StructuralPartialEq for Correspondence