Struct term_rewriting::Rule

pub struct Rule { /* fields omitted */ }

A rewrite rule equating a left-hand-side Term with one or more right-hand-side Terms.

Methods

impl Rule

pub fn new(lhs: Term, rhs: Vec<Term>) -> Option<Rule>

Construct a rewrite rule from a left-hand-side (LHS) Term with one or more right-hand-side (RHS) Terms. Returns None if the rule is not valid.

Valid rules meet two conditions:

1. lhs is an Application. This prevents a single rule from matching all possible terms
2. A Term in rhs can only use a Variable if it appears in lhs. This prevents rewrites from inventing arbitrary terms.

Trait Implementations

impl Debug for Rule

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl PartialEq for Rule

fn eq(&self, __arg_0: &Rule) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, __arg_0: &Rule) -> bool

This method tests for !=.