Struct DefEqConfig 

pub struct DefEqConfig {
    pub max_steps: u32,
    pub proof_irrelevance: bool,
    pub eta: bool,
    pub lazy_delta: bool,
    pub transparency: TransparencyMode,
}

Configuration for the definitional equality checker.

Fields

max_steps: u32

Maximum number of reduction steps before giving up.

proof_irrelevance: bool

Whether to use proof irrelevance (Props are equal).

eta: bool

Whether to check eta-expansion.

lazy_delta: bool

Whether to try lazy delta reduction.

transparency: TransparencyMode

Transparency mode for unfolding.

Implementations

impl DefEqConfig

pub fn full_transparency() -> Self

Create a config for checking definitional equality with full unfolding.

pub fn opaque() -> Self

Create a config for opaque checking (no unfolding).

pub fn no_proof_irrelevance() -> Self

Create a config with proof irrelevance disabled.

Trait Implementations

impl Clone for DefEqConfig

fn clone(&self) -> DefEqConfig

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for DefEqConfig

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for DefEqConfig

fn default() -> Self

Returns the “default value” for a type.