Struct LeanBracketedDeclarationInfo 

pub struct LeanBracketedDeclarationInfo {
    pub name: String,
    pub exists: bool,
    pub kind: Option<String>,
    pub module: Option<String>,
    pub raw_type: Option<String>,
}

Serialized declaration metadata produced inside the bracket.

Fields

name: String

exists: bool

kind: Option<String>

module: Option<String>

raw_type: Option<String>

Trait Implementations

impl Clone for LeanBracketedDeclarationInfo

fn clone(&self) -> LeanBracketedDeclarationInfo

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanBracketedDeclarationInfo

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for LeanBracketedDeclarationInfo

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for LeanBracketedDeclarationInfo

impl PartialEq for LeanBracketedDeclarationInfo

fn eq(&self, other: &LeanBracketedDeclarationInfo) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for LeanBracketedDeclarationInfo

impl<'lean> TryFromLean<'lean> for LeanBracketedDeclarationInfo

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.