Struct CorrespondenceRow 

pub struct CorrespondenceRow {
    pub lean: String,
    pub kernel: String,
    pub logos: Option<String>,
    pub kind: String,
    pub origin: String,
    pub helper_of: Option<String>,
    pub form: Option<String>,
    pub levels: Vec<(String, String)>,
    pub lines: Option<(usize, usize)>,
}

Fields

lean: String

The Lean name as Lean writes it (for a reader-introduced helper, the reader’s own name).

kernel: String

The kernel name, as the certificate declares it.

logos: Option<String>

The LOGOS name in the document, when the document declares it.

kind: String

origin: String

authored, helper, synthesized or prelude.

helper_of: Option<String>

For a helper, the authored declaration it serves.

form: Option<String>

literate, vernacular or prelude, when the document carries it.

levels: Vec<(String, String)>

Universe parameters: (kernel name, LOGOS name).

lines: Option<(usize, usize)>

The document’s 1-based inclusive line range.

Trait Implementations

impl Clone for CorrespondenceRow

fn clone(&self) -> CorrespondenceRow

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CorrespondenceRow

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for CorrespondenceRow

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for CorrespondenceRow

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

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for CorrespondenceRow

impl StructuralPartialEq for CorrespondenceRow