Struct ScopedEquivManager 

pub struct ScopedEquivManager { /* private fields */ }

A scoped equivalence manager that supports push/pop of equivalence frames.

This allows backtracking during type checking — when a unification attempt fails, all equivalences added in that scope are rolled back.

Implementations

impl ScopedEquivManager

pub fn new() -> Self

Create a new scoped manager with one initial scope.

pub fn push_scope(&mut self)

Push a new scope.

pub fn pop_scope(&mut self)

Pop the current scope, rolling back all equivalences added in it.

pub fn add_equiv(&mut self, a: &Expr, b: &Expr)

Add an equivalence in the current scope.

pub fn is_equiv(&mut self, a: &Expr, b: &Expr) -> bool

Check if two expressions are equivalent.

pub fn scope_depth(&self) -> usize

Return the current scope depth.

pub fn total_equivs(&self) -> usize

Return the total number of equivalences across all scopes.

Trait Implementations

impl Debug for ScopedEquivManager

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

Formats the value using the given formatter.

impl Default for ScopedEquivManager

fn default() -> ScopedEquivManager

Returns the “default value” for a type.