Struct DefEqChecker 

pub struct DefEqChecker<'env> { /* private fields */ }

Definitional equality checker with full optimizations.

Implementations

impl<'env> DefEqChecker<'env>

pub fn new(env: &'env Environment) -> Self

Create a new definitional equality checker.

pub fn record_fvar_type(&mut self, id: FVarId, ty: Expr)

Record the type of a free variable opened by the surrounding type checker, so Self::quick_infer_type can type it.

FVarIds are dispensed monotonically by the TypeChecker and never reused, so recorded types are stable while their variable is in scope and cached def-eq verdicts stay sound. Defensively, if a caller does re-bind an id in a way that could make them unsound — an id in scope given a different type, or an id whose binder was closed (Self::forget_fvar_type) bound again; only possible through the public TypeChecker::push_local — the caches are invalidated.

pub fn forget_fvar_type(&mut self, id: FVarId)

The binder of a free variable recorded with Self::record_fvar_type has been closed: forget its type, here and in the reducer’s mirror.

Nothing compared from here on mentions the variable, so nothing needs its type; cached verdicts that mention it are never looked up again, since its id is not dispensed again (and if a caller does bind it again, Self::record_fvar_type invalidates the caches). Without this both mirrors grow by one type per binder opened, for as long as the checker lives, and every K-like or structure-eta attempt copies all of them into a nested checker.

pub fn set_proof_irrelevance(&mut self, enabled: bool)

Disable proof irrelevance for this checker.

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

Set the transparency mode for this checker.

pub fn is_def_eq(&mut self, t: &Expr, s: &Expr) -> bool

Check if two expressions are definitionally equal.