Struct SimpResult 

pub struct SimpResult {
    pub expr: Expr,
    pub applied: Vec<Name>,
    pub changed: bool,
}

A simplified expression with a trace of applied lemma names.

Fields

expr: Expr

The simplified expression.

applied: Vec<Name>

Names of lemmas that were applied (in order).

changed: bool

Whether any change was made.

Implementations

impl SimpResult

pub fn unchanged(expr: Expr) -> Self

Simplification had no effect.

pub fn simplified(expr: Expr, applied: Vec<Name>) -> Self

Simplification succeeded.

Trait Implementations

impl Clone for SimpResult

fn clone(&self) -> SimpResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SimpResult

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

Formats the value using the given formatter.