Struct CheckConfig 

pub struct CheckConfig {
    pub check_type_is_sort: bool,
    pub check_value_type: bool,
    pub check_no_free_vars: bool,
    pub max_depth: u32,
    pub allow_axioms: bool,
}

Configuration for declaration checking.

Controls what level of checking is performed and whether certain optional checks are enabled.

Fields

check_type_is_sort: bool

Whether to check that the declared type is a sort.

check_value_type: bool

Whether to check that the value has the declared type.

check_no_free_vars: bool

Whether to check for free variables in the type and value.

max_depth: u32

Maximum depth for type inference (0 = unlimited).

allow_axioms: bool

Whether to allow axioms (false = proof-irrelevant mode).

Implementations

impl CheckConfig

pub fn new() -> Self

Create a new default configuration.

pub fn lenient() -> Self

Create a lenient configuration that skips optional checks.

pub fn strict() -> Self

Create a strict configuration that enables all checks.

Trait Implementations

impl Clone for CheckConfig

fn clone(&self) -> CheckConfig

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CheckConfig

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

Formats the value using the given formatter.

impl Default for CheckConfig

fn default() -> Self

Returns the “default value” for a type.