Struct TargetIdentity 

pub struct TargetIdentity {
    pub lean: String,
    pub kernel: String,
    pub kind: String,
    pub level_params: Vec<String>,
    pub statement: String,
    pub logos: Option<String>,
}

Fields

lean: String

The Lean name, as Lean writes it.

kernel: String

The kernel’s spelling, the certificate’s target.

kind: String

thm, def or opaque.

level_params: Vec<String>

statement: String

The statement, rendered for reading (the certificate carries the term).

logos: Option<String>

The LOGOS name in the document, when there is one.

Trait Implementations

impl Clone for TargetIdentity

fn clone(&self) -> TargetIdentity

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TargetIdentity

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for TargetIdentity

fn deserialize<__D>( __deserializer: __D, ) -> Result<TargetIdentity, <__D as Deserializer<'de>>::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for TargetIdentity

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

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

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for TargetIdentity

impl StructuralPartialEq for TargetIdentity