Struct MetaFeatures 

pub struct MetaFeatures {
    pub discr_tree: bool,
    pub whnf_cache: bool,
    pub proof_recording: bool,
    pub instance_synth: bool,
    pub congr_lemmas: bool,
}

Feature flags for the meta layer.

Fields

discr_tree: bool

Enable discrimination tree indexing for simp lemmas.

whnf_cache: bool

Enable memoization of WHNF results.

proof_recording: bool

Enable proof term recording.

instance_synth: bool

Enable instance synthesis.

congr_lemmas: bool

Enable congr-lemma automation.

Implementations

impl MetaFeatures

pub fn all_enabled() -> Self

All features enabled.

pub fn minimal() -> Self

Minimal features (fast, less complete).

pub fn any_caching(&self) -> bool

Whether at least one caching feature is enabled.

Trait Implementations

impl Clone for MetaFeatures

fn clone(&self) -> MetaFeatures

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for MetaFeatures

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

Formats the value using the given formatter.

impl Default for MetaFeatures

fn default() -> Self

Returns the “default value” for a type.