Struct ConversionChecker 

pub struct ConversionChecker { /* private fields */ }

Conversion checker for definitional equality.

Wraps a Reducer and performs structural comparison after WHNF.

Implementations

impl ConversionChecker

pub fn new() -> Self

Create a new conversion checker with default transparency.

pub fn with_transparency(mode: TransparencyMode) -> Self

Create a conversion checker with a specific transparency mode.

pub fn set_transparency(&mut self, mode: TransparencyMode)

Set the transparency mode.

pub fn transparency(&self) -> TransparencyMode

Get the current transparency mode.

pub fn is_convertible(&mut self, e1: &Expr, e2: &Expr) -> bool

Check if two expressions are convertible (without environment).

pub fn is_convertible_in_env( &mut self, e1: &Expr, e2: &Expr, env: &Environment, ) -> bool

Check if two expressions are convertible (with environment).

pub fn set_max_steps(&mut self, max: usize)

Set the maximum number of reduction steps.

pub fn max_steps(&self) -> usize

Get the maximum number of reduction steps.

Trait Implementations

impl Default for ConversionChecker

fn default() -> Self

Returns the “default value” for a type.