Struct Rederivation 

pub struct Rederivation {
    pub declaration: String,
    pub lean: String,
    pub decisions: Vec<NativeDecision>,
}

One declaration whose type or value holds re-derived leaves.

Fields

declaration: String

The kernel identity of the declaration.

lean: String

Its Lean name, as Lean writes it.

decisions: Vec<NativeDecision>

Its leaves, in export order.

Implementations

impl Rederivation

pub fn detail(&self) -> String

The disclosure, stated plainly: what Lean’s proof rested on and what LOGOS did instead.

pub fn to_json(&self) -> Value

Trait Implementations

impl Clone for Rederivation

fn clone(&self) -> Rederivation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Rederivation

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

Formats the value using the given formatter.

impl PartialEq for Rederivation

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

impl StructuralPartialEq for Rederivation