Struct Lean4CalcStep 

pub struct Lean4CalcStep {
    pub lhs: Lean4Expr,
    pub relation: String,
    pub rhs: Lean4Expr,
    pub justification: Lean4Expr,
}

One step in a calc proof.

Fields

lhs: Lean4Expr

Left-hand side expression

relation: String

Relation: =, ≤, <, ≥, >, etc.

rhs: Lean4Expr

Right-hand side expression

justification: Lean4Expr

Justification: by ... or a term

Trait Implementations

impl Clone for Lean4CalcStep

fn clone(&self) -> Lean4CalcStep

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4CalcStep

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

Formats the value using the given formatter.

impl Display for Lean4CalcStep

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

Formats the value using the given formatter.

impl PartialEq for Lean4CalcStep

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