Enum SimpDirection 

pub enum SimpDirection {
    Forward,
    Reversed,
}

How a committed lemma may join a simp set. Discovery commits equations in enumeration orientation, so usability as a rewrite rule is a property to RECOVER, not assume.

Variants

Forward

LHS head is a program fn (count x2 (x0 ++ x1) = plus …, decode (encode xs) = xs): use as-is — rewrites toward decomposed/builtin normal form.

Reversed

LHS is builtin-headed but the RHS head is a program fn (the trivia (x0 ++ x1) = append x0 x1): use as ← name — rewrites the opaque program fn INTO its builtin shape (an unfolding equation the fn’s own def can’t provide when its recursion is stuck on a symbolic arg).

Trait Implementations

impl Clone for SimpDirection

fn clone(&self) -> SimpDirection

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Copy for SimpDirection

impl Debug for SimpDirection

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

Formats the value using the given formatter.

impl Eq for SimpDirection

impl PartialEq for SimpDirection

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