Struct Rule 

pub struct Rule {
    pub lhs: Term,
    pub rhs: Term,
}

A rewrite rule lhs → rhs.

Variables in lhs range over Term::Var(i). The rule is valid when every variable in rhs also occurs in lhs.

Fields

lhs: Term

rhs: Term

Implementations

impl Rule

pub fn new(lhs: Term, rhs: Term) -> Self

Creates a new rewrite rule.

pub fn is_valid(&self) -> bool

Returns true if every variable in rhs occurs in lhs.

pub fn is_left_linear(&self) -> bool

Returns true if lhs is linear (each variable occurs at most once).

pub fn rename(&self, offset: u32) -> Rule

Returns a renamed copy of this rule with variables shifted by offset.

Trait Implementations

impl Clone for Rule

fn clone(&self) -> Rule

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Rule

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

Formats the value using the given formatter.