Struct Reducer 

pub struct Reducer { /* private fields */ }

Reduction context with caching.

Implementations

impl Reducer

pub fn new() -> Self

Create a new reducer with default settings.

pub fn with_max_depth(max_depth: u32) -> Self

Create a reducer with custom max depth.

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

Set the transparency mode.

pub fn clear_cache(&mut self)

Clear the cache (call between declarations).

pub fn whnf(&mut self, expr: &Expr) -> Expr

Reduce an expression to Weak Head Normal Form.

This implements all reduction rules except delta (which needs environment).

pub fn whnf_delta<F>(&mut self, expr: &Expr, lookup: &F) -> Expr

where F: Fn(&Name) -> Option<(Expr, ReducibilityHint)>,

Reduce to WHNF with delta-reduction (constant unfolding).

This requires environment access to look up definitions.

pub fn whnf_env(&mut self, expr: &Expr, env: &Environment) -> Expr

Full WHNF with environment-aware reductions.

Performs: beta, zeta, delta, iota (recursor), projection, nat/string ops.

pub fn is_alpha_equiv(e1: &Expr, e2: &Expr) -> bool

Check if two expressions are alpha-equivalent (syntactically equal).

Trait Implementations

impl Default for Reducer

fn default() -> Self

Returns the “default value” for a type.