Struct ExtendedSimpSet 

pub struct ExtendedSimpSet {
    pub lemmas: Vec<(String, u64)>,
    pub erased: Vec<String>,
}

A simp set extended with custom lemmas and priorities.

Fields

lemmas: Vec<(String, u64)>

Lemma names and priorities in this simp set.

erased: Vec<String>

Erased lemma names.

Implementations

impl ExtendedSimpSet

pub fn new() -> Self

Create an empty simp set.

pub fn add_lemma(&mut self, name: &str, priority: u64)

Add a lemma with a given priority.

pub fn erase_lemma(&mut self, name: &str)

Erase a lemma by name.

pub fn is_active(&self, name: &str) -> bool

Check if a lemma name is active (added but not erased).

pub fn sorted_lemmas(&self) -> Vec<(String, u64)>

Sort lemmas by descending priority.

pub fn active_count(&self) -> usize

Total number of active lemmas.

Trait Implementations

impl Default for ExtendedSimpSet

fn default() -> Self

Returns the “default value” for a type.