Enum STerm 

pub enum STerm {
    Lit(i64),
    Var(i64),
    Name(String),
    App(Box<STerm>, Box<STerm>),
}

Simplified representation of Syntax terms for rewriting.

This is a flattened version of the kernel’s Term type, specialized for the Syntax deep embedding. Unlike Term, STerm is designed for efficient pattern matching and rewriting during simplification.

The correspondence is:

• Term::App(Global("SLit"), Lit(n)) -> STerm::Lit(n)
• Term::App(Global("SVar"), Lit(i)) -> STerm::Var(i)
• Term::App(Global("SName"), Lit(s)) -> STerm::Name(s)
• Term::App(App(Global("SApp"), f), a) -> STerm::App(f, a)

Variants

Lit(i64)

Integer literal from SLit n.

Var(i64)

De Bruijn variable from SVar i.

Name(String)

Named constant or function symbol from SName s.

App(Box<STerm>, Box<STerm>)

Function application from SApp f a.

Trait Implementations

impl Clone for STerm

fn clone(&self) -> STerm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for STerm

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

Formats the value using the given formatter.

impl Hash for STerm

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for STerm

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

impl StructuralPartialEq for STerm