Struct Converter 

pub struct Converter { /* private fields */ }

Conversion checker with WHNF evaluation

Implementations

impl Converter

pub fn new() -> Self

Create a new converter with default fuel

pub fn with_fuel(fuel: u32) -> Self

Create a converter with custom fuel

pub fn is_def_eq( &mut self, arena: &mut Arena, env: &Environment, ctx: &Context, t1: TermId, t2: TermId, ) -> Result<bool>

Check if two terms are definitionally equal

pub fn whnf( &mut self, arena: &mut Arena, env: &Environment, ctx: &Context, term: TermId, ) -> Result<TermId>

Reduce a term to weak head normal form

pub fn substitute( &mut self, arena: &mut Arena, term: TermId, idx: u32, replacement: TermId, ) -> Result<TermId>

Substitute a term in another term subst(term, idx, replacement) replaces variable #idx with replacement

pub fn stats(&self) -> &ConversionStats

Get conversion statistics

pub fn clear_cache(&self)

Clear the WHNF cache

pub fn reset_fuel(&mut self)

Reset fuel to default

Trait Implementations

impl Default for Converter

fn default() -> Self

Returns the “default value” for a type.