Struct SimpLemma 

pub struct SimpLemma {
    pub name: Name,
    pub lhs: Expr,
    pub rhs: Expr,
    pub direction: SimpDirection,
    pub priority: i32,
}

A single simp lemma: a conditional rewrite rule lhs = rhs.

Fields

name: Name

Name of the lemma.

lhs: Expr

Left-hand side pattern.

rhs: Expr

Right-hand side replacement.

direction: SimpDirection

Rewrite direction.

priority: i32

Priority (higher = preferred).

Implementations

impl SimpLemma

pub fn forward(name: Name, lhs: Expr, rhs: Expr) -> Self

Create a forward simp lemma.

pub fn backward(name: Name, lhs: Expr, rhs: Expr) -> Self

Create a backward simp lemma.

pub fn reversed(self) -> Self

Swap the simp lemma direction.

pub fn effective_lhs(&self) -> &Expr

Return the effective LHS (after direction is applied).

pub fn effective_rhs(&self) -> &Expr

Return the effective RHS (after direction is applied).

Trait Implementations

impl Clone for SimpLemma

fn clone(&self) -> SimpLemma

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SimpLemma

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

Formats the value using the given formatter.