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 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.