Struct CalcStep 

pub struct CalcStep {
    pub lhs: Located<SurfaceExpr>,
    pub rel: String,
    pub rhs: Located<SurfaceExpr>,
    pub proof: Located<SurfaceExpr>,
}

A single step in a calc proof expression.

Example:

calc a = b := proof1
     _ < c := proof2

Fields

lhs: Located<SurfaceExpr>

Left-hand side of the step.

rel: String

Relation symbol (e.g., =, <, <=).

rhs: Located<SurfaceExpr>

Right-hand side of the step.

proof: Located<SurfaceExpr>

Proof/justification for this step.

Implementations

impl CalcStep

pub fn new( lhs: Located<SurfaceExpr>, rel: String, rhs: Located<SurfaceExpr>, proof: Located<SurfaceExpr>, ) -> Self

Create a new calc step.

Trait Implementations

impl Clone for CalcStep

fn clone(&self) -> CalcStep

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CalcStep

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

Formats the value using the given formatter.

impl PartialEq for CalcStep

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